mul_inv_eq_mul_inv_iff — Mathlib

English

The MonoidWithZero version of inv_mul_eq_inv_mul_iff_mul_eq_mul: b⁻¹ a = d⁻¹ c iff d a = b c, under nonzero assumptions and commutativity.

Русский

Версия для MonoidWithZero: b⁻¹ a = d⁻¹ c эквивалентно d a = b c при условии не нулей и коммутативности.

LaTeX

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

Lean4

/-- The `MonoidWithZero` version of `mul_inv_eq_mul_inv_iff_mul_eq_mul`. -/
protected theorem mul_inv_eq_mul_inv_iff (hbd : Commute b d) (hb : b ≠ 0) (hd : d ≠ 0) :
    a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b :=
  hbd.mul_inv_eq_mul_inv_iff_of_isUnit hb.isUnit hd.isUnit

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