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.lean.

source
theorem Invertible.ne_zero {α : Type u} [MulZeroOneClass α] (a : α) [Nontrivial α] [Invertible a] :
a ≠ 0
source
@[instance 100]
instance Invertible.toNeZero {α : Type u} [MulZeroOneClass α] [Nontrivial α] (a : α) [Invertible a] :
NeZero a
source
@[simp]
theorem Ring.inverse_invertible {α : Type u} [MonoidWithZero α] (x : α) [Invertible x] :
inverse x = ⅟ x

A variant of Ring.inverse_unit.

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

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

Equations
    Instances For
      source
      @[simp]
      theorem invOf_eq_inv {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
      ⅟ a = a⁻¹
      source
      @[simp]
      theorem inv_mul_cancel_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
      a⁻¹ * a = 1
      source
      @[simp]
      theorem mul_inv_cancel_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
      a * a⁻¹ = 1
      source
      def invertibleInv {α : Type u} [GroupWithZero α] {a : α} [Invertible a] :
      Invertible a⁻¹

      a is the inverse of a⁻¹

      Equations
        Instances For
          source
          @[simp]
          theorem div_mul_cancel_of_invertible {α : Type u} [GroupWithZero α] (a b : α) [Invertible b] :
          a / b * b = a
          source
          @[simp]
          theorem mul_div_cancel_of_invertible {α : Type u} [GroupWithZero α] (a b : α) [Invertible b] :
          a * b / b = a
          source
          @[simp]
          theorem div_self_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
          a / a = 1
          source
          def invertibleDiv {α : Type u} [GroupWithZero α] (a b : α) [Invertible a] [Invertible b] :
          Invertible (a / b)

          b / a is the inverse of a / b

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