val_inv — Mathlib

English

If x is a unit in a monoid with involution and x is star-normal, then x^{-1} is star-normal.

Русский

Если x — единица в моноиде с операцией звезды и x звёздно-нормален, то x^{-1} звёздно-нормален.

LaTeX

$$$\forall R\,[Monoid\; R]\,[StarMul\; R]\;{x : Units\; R},\; IsStarNormal\,(x : R)\;\Rightarrow\; IsStarNormal$(x)^{-1} : R$$$$

Lean4

protected instance val_inv [Monoid R] [StarMul R] {x : Rˣ} [IsStarNormal (x : R)] : IsStarNormal (↑x⁻¹ : R) where
  star_comm_self := by simpa [← Units.coe_star_inv, -Commute.units_val_iff] using star_comm_self

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