div_eq_div_iff — Mathlib

English

If b and d commute with nonzero b,d, then a b⁻¹ = c d⁻¹ is equivalent to a d = c b.

Русский

Если b и d коммутируют и не нули, то a b⁻¹ = c d⁻¹ эквивалентно a d = c b.

LaTeX

$$\\forall a,b,c,d, hbd: Commute(b,d), hb: b ≠ 0, hd: d ≠ 0, \\\\; a b^{-1} = c d^{-1} \\iff a d = c b$$

Lean4

/-- The `MonoidWithZero` version of `div_eq_div_iff_mul_eq_mul`. -/
protected theorem div_eq_div_iff (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c * b :=
  hbd.div_eq_div_iff_of_isUnit hb.isUnit hd.isUnit

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