English
If a/b = c/d in a DivisionMonoid with b,d units that commute, then a d = c b, and conversely.
Русский
Если a/b = c/d в делимом полугруппе, где b,d являются единицами и коммутируют, тогда a d = c b, и обратно.
LaTeX
$$$\\\\forall {M} [DivisionMonoid M] \\\\ (Commute b d) \\\\Rightarrow \\\\left( \\\\operatorname{Eq}(a / b, c / d) \\\\Rightarrow \\\\operatorname{Eq}(a d, c b) \right) \\\\land \\\\left( \\\\operatorname{Eq}(a d, c b) \\\\Rightarrow \\\\operatorname{Eq}(a / b, c / d) \right)$$
Lean4
@[to_additive]
theorem inv_mul_eq_inv_mul_iff_of_isUnit (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
b⁻¹ * a = d⁻¹ * c ↔ d * a = b * c := by
rw [← (hd.mul hb).mul_right_inj, ← mul_assoc, mul_assoc d, hb.mul_inv_cancel, mul_one, ← mul_assoc, mul_assoc d,
hbd.symm.left_comm, hd.mul_inv_cancel, mul_one]
