English
For any group G with StarMul, the unitary elements form a subgroup of G.
Русский
Для любой группы G со StarMul унитарные элементы образуют подгруппу G.
LaTeX
$$$ \text{unitary}(G) \le G $ with inverse given by star$$
Lean4
/-- `unitary` as a `Subgroup` of a group.
Note the group structure on this type is not defeq to the one on `unitary`.
This situation naturally arises when considering the unitary elements as a
subgroup of the group of units of a star monoid. -/
def unitarySubgroup : Subgroup G where
toSubmonoid := unitary G
inv_mem' := unitary.inv_mem