mul_inv_eq_mul_inv_iff_of_isUnit — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_inv_eq_mul_inv_iff_of_isUnit (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
    a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b := by rw [← div_eq_mul_inv, ← div_eq_mul_inv, hbd.div_eq_div_iff_of_isUnit hb hd]

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