unitarySubgroup — Mathlib

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

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