mul_eq_mul_of_div_eq_div — Mathlib

English

Let b,d be units in α. If a/b = c/d, then a d = c b.

Русский

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

LaTeX

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

Lean4

@[to_additive]
protected theorem mul_eq_mul_of_div_eq_div (hb : IsUnit b) (hd : IsUnit d) (a c : α) (h : a / b = c / d) :
    a * d = c * b := by rw [← mul_one a, ← hb.div_self, ← mul_comm_div, h, div_mul_eq_mul_div, hd.div_mul_cancel]

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