Documentation

Mathlib.Algebra.Invertible.GroupWithZero

Theorems about invertible elements in a GroupWithZero #

We intentionally keep imports minimal here as this file is used by Mathlib.Tactic.NormNum.

theorem nonzero_of_invertible {α : Type u} [MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] :
a 0
instance Invertible.ne_zero {α : Type u} [MulZeroOneClass α] [Nontrivial α] (a : α) [Invertible a] :
Equations
def invertibleOfNonzero {α : Type u} [GroupWithZero α] {a : α} (h : a 0) :

a⁻¹ is an inverse of a if a ≠ 0

Equations
Instances For
    @[simp]
    theorem invOf_eq_inv {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
    @[simp]
    theorem inv_mul_cancel_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
    a⁻¹ * a = 1
    @[simp]
    theorem mul_inv_cancel_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
    a * a⁻¹ = 1
    def invertibleInv {α : Type u} [GroupWithZero α] {a : α} [Invertible a] :

    a is the inverse of a⁻¹

    Equations
    • invertibleInv = { invOf := a, invOf_mul_self := (_ : a * a⁻¹ = 1), mul_invOf_self := (_ : a⁻¹ * a = 1) }
    Instances For