div_sub_div — Mathlib

English

Let b and c commute, and b and d commute, with b ≠ 0 and d ≠ 0. Then a/b − c/d = (ad − bc)/(bd).

Русский

Пусть b и c коммутируют, и b коммутирует с d, при условии b ≠ 0 и d ≠ 0. Тогда a/b − c/d = (ad − bc)/(bd).

LaTeX

$$$\\frac{a}{b} - \\frac{c}{d} = \\frac{a d - b c}{b d}$$$

Lean4

protected theorem div_sub_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
  simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd

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