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] : NeZero a

Equations

• @Invertible.ne_zero = @Invertible.ne_zero.proof_1

def invertibleOfNonzero {α : Type u} [GroupWithZero α] {a : α} (h : a ≠ 0) : Invertible a

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

Equations

• invertibleOfNonzero h = { invOf := a⁻¹, invOf_mul_self := (_ : a⁻¹ * a = 1), mul_invOf_self := (_ : a * a⁻¹ = 1) }

@[simp]

theorem invOf_eq_inv {α : Type u} [GroupWithZero α] (a : α) [Invertible a] : ⅟a = 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] : Invertible a⁻¹

a is the inverse of a⁻¹

Equations

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