Theorems about invertible elements in a GroupWithZero

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

theorem Invertible.ne_zero {α : Type u} [MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] : a ≠ 0

@[instance 100]

instance Invertible.toNeZero {α : Type u} [MulZeroOneClass α] [Nontrivial α] (a : α) [Invertible a] : NeZero a

@[simp]

theorem Ring.inverse_invertible {α : Type u} [MonoidWithZero α] (x : α) [Invertible x] : inverse x = ⅟ x

A variant of Ring.inverse_unit.

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

@[simp]

theorem div_mul_cancel_of_invertible {α : Type u} [GroupWithZero α] (a b : α) [Invertible b] : a / b * b = a

@[simp]

theorem mul_div_cancel_of_invertible {α : Type u} [GroupWithZero α] (a b : α) [Invertible b] : a * b / b = a

@[simp]

theorem div_self_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] : a / a = 1

def invertibleDiv {α : Type u} [GroupWithZero α] (a b : α) [Invertible a] [Invertible b] : Invertible (a / b)

b / a is the inverse of a / b

Equations

• invertibleDiv a b = { invOf := b / a, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem invOf_div {α : Type u} [GroupWithZero α] (a b : α) [Invertible a] [Invertible b] [Invertible (a / b)] : ⅟ (a / b) = b / a