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
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 := , mul_invOf_self := }
    Instances For
      @[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 := }
      Instances For
        theorem invOf_div {α : Type u} [GroupWithZero α] (a : α) (b : α) [Invertible a] [Invertible b] [Invertible (a / b)] :
        (a / b) = b / a