div_eq_div_iff_of_isUnit — Mathlib

English

If b and d commute and are units in a DivisionMonoid, then a b^{-1} = c d^{-1} iff a d = c b.

Русский

Если b и d коммутируют и являются единицами в делимом полугруппе, то a b^{-1} = c d^{-1} тогда и только тогда, когда a d = c b.

LaTeX

$$$\\\\forall {M} [DivisionMonoid M] \\\\ (\\\\operatorname{Commute} b d) \\\\Rightarrow \\\\left( a b^{-1} = c d^{-1} \\\\iff a d = c b \\right)$$$

Lean4

@[to_additive]
theorem div_eq_div_iff_of_isUnit (hbd : Commute b d) (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, hbd.right_comm, hd.div_mul_cancel]

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