English
The unitary subgroup of the units is equivalent to the unitary elements of the monoid.
Русский
Унитарная подгруппа единиц эквивалентна унитарным элементам моноида.
LaTeX
$$$\\mathrm{unitarySubgroup}(M^{\\times}) \\simeq_* \\mathrm{unitary}(M)$$$
Lean4
/-- The unitary subgroup of the units is equivalent to the unitary elements of the monoid. -/
@[simps!]
def _root_.unitarySubgroupUnitsEquiv {M : Type*} [Monoid M] [StarMul M] : unitarySubgroup Mˣ ≃* unitary M
where
toFun x := ⟨x.val, congr_arg Units.val x.prop.1, congr_arg Units.val x.prop.2⟩
invFun x := ⟨⟨x, star x, x.prop.2, x.prop.1⟩, Units.ext x.prop.1, Units.ext x.prop.2⟩
map_mul' _ _ := rfl
left_inv _ := Subtype.ext <| Units.ext rfl
right_inv _ := rfl
