English
If R is a monoid with an involution, then the group of units Rˣ carries a natural star-structure defined by star u using star on the underlying element and star on its inverse.
Русский
Если R — моноид с операцией звезды, то множество обратимых элементов Rˣ естественным образом оборудуется структурой звезды: для единицы u задается star(u) с использованием звезды на самих элементах и на их обратном.
LaTeX
$$$\text{If } R \text{ is a monoid with } \star, \; \text{then } (R^{\times}, \star) \text{ is a star-monoid with } \star(u) = \star u, \; \star(u)^{-1} = \star(u^{-1}).$$$
Lean4
instance : StarMul Rˣ
where
star
u :=
{ val := star u
inv := star ↑u⁻¹
val_inv := (star_mul _ _).symm.trans <| (congr_arg star u.inv_val).trans <| star_one _
inv_val := (star_mul _ _).symm.trans <| (congr_arg star u.val_inv).trans <| star_one _ }
star_involutive _ := Units.ext (star_involutive _)
star_mul _ _ := Units.ext (star_mul _ _)
