div_eq_div_iff — Mathlib

English

Let b,d be units in α. Then a/b = c/d if and only if a d = c b.

Русский

Пусть b,d — единицы в α. Тогда a/b = c/d тогда же, как ad = cb.

LaTeX

$$$$ \\forall b,d \\in \\alpha^{\\times},\\ a,c \\in \\alpha:\\ \\frac{a}{b} = \\frac{c}{d} \\iff a d = c b. $$$$

Lean4

@[to_additive]
protected theorem div_eq_div_iff (hb : IsUnit b) (hd : IsUnit d) : a / b = c / d ↔ a * d = c * b := by
  rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm, hd.div_mul_cancel]

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