invOf_sub_invOf — Mathlib

English

For a ring R with inverses a,b, ⅟a − ⅟b = ⅟a * (b − a) * ⅟b.

Русский

Для кольца R с обратимыми a,b: ⅟a − ⅟b = ⅟a * (b − a) * ⅟b.

LaTeX

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

Lean4

/-- A version of `inv_sub_inv'` for `invOf`. -/
theorem invOf_sub_invOf [Ring R] (a b : R) [Invertible a] [Invertible b] : ⅟a - ⅟b = ⅟a * (b - a) * ⅟b := by
  rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]

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