one_div_add_one_div — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem one_div_add_one_div (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
    1 / a + 1 / b = (a + b) / (a * b) := by rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]

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