Documentation

Mathlib.Algebra.GroupWithZero.Invertible

Theorems about invertible elements in a GroupWithZero #

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

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

Alias of Invertible.ne_zero.

@[instance 100]
instance Invertible.toNeZero {α : Type u} [MulZeroOneClass α] [Nontrivial α] (a : α) [Invertible a] :
Equations
  • =
@[simp]
theorem Ring.inverse_invertible {α : Type u} [MonoidWithZero α] (x : α) [Invertible x] :

A variant of Ring.inverse_unit.

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

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

Equations
@[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 := , 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] :

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