Theorems about additively and multiplicatively invertible elements in rings

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.

@[simp]

theorem AddUnits.val_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) : ↑(x.mulLeft y) = y * ↑x

@[simp]

theorem AddUnits.val_neg_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) : ↑(-x.mulLeft y) = y * x.neg

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.

@[simp]

theorem AddUnits.val_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) : ↑(x.mulRight y) = ↑x * y

@[simp]

theorem AddUnits.val_neg_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R) : ↑(-x.mulRight y) = x.neg * y

theorem AddUnits.neg_mulLeft {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R} : -x.mulLeft y = (-x).mulLeft y

theorem AddUnits.neg_mulRight {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R} : -x.mulRight y = (-x).mulRight y

@[deprecated AddUnits.neg_mulLeft (since := "2025-10-03")]

theorem AddUnits.neg_mul_left {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R} : -x.mulLeft y = (-x).mulLeft y

Alias of AddUnits.neg_mulLeft.

@[deprecated AddUnits.neg_mulRight (since := "2025-10-03")]

theorem AddUnits.neg_mul_right {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : AddUnits R} {y : R} : -x.mulRight y = (-x).mulRight y

Alias of AddUnits.neg_mulRight.

theorem AddUnits.neg_mul_eq_mul_neg {R : Type u_1} [NonUnitalNonAssocSemiring R] {x y : AddUnits R} : ↑(-x) * ↑y = ↑x * ↑(-y)

theorem AddUnits.neg_mul_neg {R : Type u_1} [NonUnitalNonAssocSemiring R] {x y : AddUnits R} : ↑(-x) * ↑(-y) = ↑x * ↑y

theorem IsAddUnit.mul_left {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : R} (h : IsAddUnit x) (y : R) : IsAddUnit (y * x)

theorem IsAddUnit.mul_right {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : R} (h : IsAddUnit x) (y : R) : IsAddUnit (x * y)

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

-⅟a is the inverse of -a

@[simp]

theorem invOf_neg {R : Type u_1} [Monoid R] [HasDistribNeg R] (a : R) [Invertible a] [Invertible (-a)] : ⅟(-a) = -⅟a

@[simp]

theorem one_sub_invOf_two {R : Type u_1} [Ring R] [Invertible 2] : 1 - ⅟2 = ⅟2

@[simp]

theorem invOf_two_add_invOf_two {R : Type u_1} [NonAssocSemiring R] [Invertible 2] : ⅟2 + ⅟2 = 1

theorem pos_of_invertible_cast {R : Type u_1} [NonAssocSemiring R] [Nontrivial R] (n : ℕ) [Invertible ↑n] : 0 < n

theorem invOf_add_invOf {R : Type u_1} [Semiring R] (a b : R) [Invertible a] [Invertible b] : ⅟a + ⅟b = ⅟a * (a + b) * ⅟b

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.

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

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

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

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.

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.