invOf_add_invOf — Mathlib

English

For a ring R and elements a,b with inverses, ⅟a + ⅟b = ⅟a * (a + b) * ⅟b.

Русский

Для кольца R и элементов a,b с обратимыми, ⅟a + ⅟b = ⅟a * (a + b) * ⅟b.

LaTeX

$$⅟a + ⅟b = ⅟a * (a + b) * ⅟b$$

Lean4

theorem invOf_add_invOf [Semiring R] (a b : R) [Invertible a] [Invertible b] : ⅟a + ⅟b = ⅟a * (a + b) * ⅟b := by
  rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]

Похожие утверждения