Documentation

Mathlib.Algebra.Ring.Invertible

Theorems about additively and multiplicatively invertible elements in rings #

source
def AddUnits.mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) :
AddUnits R

Multiplying an additive unit from the left produces another additive unit.

Equations
  • x.mulLeft y = { val := y * ↑x, neg := y * x.neg, val_neg := ⋯, neg_val := ⋯ }
Instances For
    source
    @[simp]
    theorem AddUnits.val_neg_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) :
    ↑(-x.mulLeft y) = y * x.neg
    source
    @[simp]
    theorem AddUnits.val_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) :
    ↑(x.mulLeft y) = y * ↑x
    source
    def AddUnits.mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) :
    AddUnits R

    Multiplying an additive unit from the right produces another additive unit.

    Equations
    • x.mulRight y = { val := ↑x * y, neg := x.neg * y, val_neg := ⋯, neg_val := ⋯ }
    Instances For
      source
      @[simp]
      theorem AddUnits.val_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) :
      ↑(x.mulRight y) = ↑x * y
      source
      @[simp]
      theorem AddUnits.val_neg_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) :
      ↑(-x.mulRight y) = x.neg * y
      source
      theorem AddUnits.neg_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R} :
      -x.mulLeft y = (-x).mulLeft y
      source
      theorem AddUnits.neg_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R} :
      -x.mulRight y = (-x).mulRight y
      source
      theorem AddUnits.neg_mul_eq_mul_neg {R : Type u_1} [NonUnitalNonAssocSemiring R] {x y : AddUnits R} :
      ↑(-x) * ↑y = ↑x * ↑(-y)
      source
      theorem AddUnits.neg_mul_neg {R : Type u_1} [NonUnitalNonAssocSemiring R] {x y : AddUnits R} :
      ↑(-x) * ↑(-y) = ↑x * ↑y
      source
      theorem IsAddUnit.mul_left {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : R} (h : IsAddUnit x) (y : R) :
      IsAddUnit (y * x)
      source
      theorem IsAddUnit.mul_right {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : R} (h : IsAddUnit x) (y : R) :
      IsAddUnit (x * y)
      source
      @[instance_reducible]
      def invertibleNeg {R : Type u_1} [Mul R] [One R] [HasDistribNeg R] (a : R) [Invertible a] :
      Invertible (-a)

      -⅟a is the inverse of -a

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

        A version of inv_sub_inv' for invOf.

        source
        theorem neg_add_eq_mul_invOf_mul_same_iff {R : Type u_1} [Ring R] {a b : R} [Invertible a] [Invertible b] :
        -(b + a) = a * ⅟b * a ↔ -1 = ⅟a * b + ⅟b * a
        source
        theorem neg_one_eq_invOf_mul_add_invOf_mul_iff {R : Type u_1} [Ring R] {a b : R} [Invertible a] [Invertible b] [Invertible (a + b)] :
        ⅟(a + b) = ⅟a + ⅟b ↔ -1 = ⅟a * b + ⅟b * a
        source
        theorem eq_of_invOf_add_eq_invOf_add_invOf {R : Type u_1} [Ring R] {a b : R} [Invertible a] [Invertible b] [Invertible (a + b)] (h : ⅟(a + b) = ⅟a + ⅟b) :
        a * ⅟b * a = b * ⅟a * b
        source
        theorem Ring.inverse_add_inverse {R : Type u_1} [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.

        source
        theorem Ring.inverse_sub_inverse {R : Type u_1} [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.