Documentation

Mathlib.Algebra.Ring.Invertible

Theorems about invertible elements in rings #

def invertibleNeg {R : Type u} [Mul R] [One R] [HasDistribNeg R] (a : R) [Invertible a] :

-⅟a is the inverse of -a

Equations
    Instances For
      @[simp]
      theorem invOf_neg {R : Type u} [Monoid R] [HasDistribNeg R] (a : R) [Invertible a] [Invertible (-a)] :
      (-a) = - a
      @[simp]
      theorem one_sub_invOf_two {R : Type u} [Ring R] [Invertible 2] :
      1 - 2 = 2
      @[simp]
      theorem pos_of_invertible_cast {R : Type u} [NonAssocSemiring R] [Nontrivial R] (n : ) [Invertible n] :
      0 < n
      theorem invOf_add_invOf {R : Type u} [Semiring R] (a b : R) [Invertible a] [Invertible b] :
      a + b = a * (a + b) * b
      theorem invOf_sub_invOf {R : Type u} [Ring R] (a b : R) [Invertible a] [Invertible b] :
      a - b = a * (b - a) * b

      A version of inv_sub_inv' for invOf.

      theorem Ring.inverse_add_inverse {R : Type u} [Semiring R] {a b : R} (h : IsUnit a IsUnit b) :
      inverse a + inverse b = inverse a * (a + b) * inverse b

      A version of inv_add_inv' for Ring.inverse.

      theorem Ring.inverse_sub_inverse {R : Type u} [Ring R] {a b : R} (h : IsUnit a IsUnit b) :
      inverse a - inverse b = inverse a * (b - a) * inverse b

      A version of inv_sub_inv' for Ring.inverse.