inv_add_inv — Mathlib

English

If a and b commute and are nonzero, then a^{-1} + b^{-1} = (a + b)/(ab).

Русский

Если a и b коммутируют и ненулевые, то a^{-1} + b^{-1} = (a+b)/(ab).

LaTeX

$$$$a^{-1} + b^{-1} = \\frac{a+b}{ab} \quad (a,b\\neq 0,\\; \\text{Commute}(a,b)).$$$$

Lean4

protected theorem inv_add_inv (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = (a + b) / (a * b) := by
  rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]

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