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

• ⋯ = ⋯

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 := ⋯, mul_invOf_self := ⋯ }

@[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 := ⋯, mul_invOf_self := ⋯ }