Theorems about invertible elements in rings

def invertibleNeg {α : Type u} [Mul α] [One α] [HasDistribNeg α] (a : α) [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 {α : Type u} [Monoid α] [HasDistribNeg α] (a : α) [Invertible a] [Invertible (-a)] : ⅟(-a) = -⅟a

@[simp]

theorem one_sub_invOf_two {α : Type u} [Ring α] [Invertible 2] : 1 - ⅟2 = ⅟2

@[simp]

theorem invOf_two_add_invOf_two {α : Type u} [NonAssocSemiring α] [Invertible 2] : ⅟2 + ⅟2 = 1

theorem pos_of_invertible_cast {α : Type u} [Semiring α] [Nontrivial α] (n : ℕ) [Invertible ↑n] : 0 < n

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

theorem invOf_sub_invOf {α : Type u} [Ring α] (a : α) (b : α) [Invertible a] [Invertible b] : ⅟a - ⅟b = ⅟a * (b - a) * ⅟b

A version of inv_sub_inv' for invOf.

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

A version of inv_add_inv' for Ring.inverse.

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

A version of inv_sub_inv' for Ring.inverse.