Theorems about invertible elements in rings

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

-⅟a is the inverse of -a

Equations

• invertibleNeg a = { invOf := -⅟ a, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[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 invOf_two_add_invOf_two {R : Type u} [NonAssocSemiring R] [Invertible 2] : ⅟ 2 + ⅟ 2 = 1

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.