inv_mul_mem_unitary — Mathlib

English

In a star monoid, the product a^{-1} · b of units is unitary iff a · star(a) = b · star(b).

Русский

В звёздном моноиде произведение единиц a^{-1} · b унитарно тогда и только тогда, когда a · star(a) = b · star(b).

LaTeX

$$$ (a^{-1} \cdot b) \in \mathrm{unitary}(R) \iff a \star a = b \star b $$$

Lean4

/-- In a star monoid, the product `a⁻¹ * b` of units is unitary if `a * star a = b * star b`. -/
protected theorem _root_.Units.inv_mul_mem_unitary (a b : Rˣ) : (a⁻¹ * b : R) ∈ unitary R ↔ a * star a = b * star b :=
  by simp [← inv_mul_mem_iff, Units.unitary_eq]

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