div_add_div — Mathlib

English

If b and c commute and b,d commute with the same nonzero properties, then a/b + c/d = (ad + bc) / (bd).

Русский

Если b и c коммутируют, и b и d коммутируют, то a/b + c/d = (ad+bc)/(bd).

LaTeX

$$$$a/b + c/d = (a d + b c)/(b d)$$ при $\operatorname{Commute}(b,c)$, $\operatorname{Commute}(b,d)$, $b\neq 0$, $d\neq 0$.$$

Lean4

protected theorem div_add_div (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
    a / b + c / d = (a * d + b * c) / (b * d) := by
  rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]

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