mul_inv_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 `star a * a = star b * b`. -/
protected theorem _root_.Units.mul_inv_mem_unitary (a b : Rˣ) : (a * b⁻¹ : R) ∈ unitary R ↔ star a * a = star b * b :=
  by simp [← mul_inv_mem_iff, Units.unitary_eq]

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