English
There is a star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of the underlying star monoids.
Русский
Существует изоморфизм между унитарными подгруппами, индуцированный изоморфизмом звездных моноидов низшей структуры.
LaTeX
$$$\\mathrm{mapEquiv} : (\\mathrm{unitary} R) \\simeq_* (\\mathrm{unitary} S)$$$
Lean4
/-- The star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of
the underlying star monoids. -/
@[simps]
def mapEquiv (f : R ≃⋆* S) : unitary R ≃⋆* unitary S :=
{ map f.toStarMonoidHom with
toFun := map f.toStarMonoidHom
invFun := map f.symm.toStarMonoidHom
left_inv := fun _ ↦ Subtype.ext <| f.left_inv _
right_inv := fun _ ↦ Subtype.ext <| f.right_inv _ }
