inv_mul_eq_inv_mul_iff — Mathlib

English

The MonoidWithZero version of inv_mul_eq_inv_mul_iff: b⁻¹ · a = d⁻¹ · c iff d · a = b · c.

Русский

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

LaTeX

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

Lean4

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

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