mul_inv_eq_mul_inv_iff — Mathlib

English

Let b,d be units. Then a·b^{-1} = c·d^{-1} if and only if a·d = c·b.

Русский

Пусть b,d — единицы. Тогда a·b^{-1} = c·d^{-1} тогда и только тогда, когда a·d = c·b.

LaTeX

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

Lean4

@[to_additive]
protected theorem mul_inv_eq_mul_inv_iff (hb : IsUnit b) (hd : IsUnit d) : a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b := by
  rw [← div_eq_mul_inv, ← div_eq_mul_inv, hb.div_eq_div_iff hd]

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