inv_sub_inv — Mathlib

English

Let a and b commute, with a ≠ 0 and b ≠ 0. Then a⁻¹ − b⁻¹ = (b − a)/(a b).

Русский

Пусть a и b коммутируют, a ≠ 0, b ≠ 0. Тогда a⁻¹ − b⁻¹ = (b − a)/(a b).

LaTeX

$$$a^{-1} - b^{-1} = \\dfrac{b - a}{a b}$, при $a \\neq 0$, $b \\neq 0$ и $ab=ba$$$

Lean4

protected theorem inv_sub_inv (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ - b⁻¹ = (b - a) / (a * b) := by
  simp only [inv_eq_one_div, (Commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]

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