unitary R is a topological group #
In a topological star monoid, the unitary group is a topological group.
instance
instContinuousStarSubtypeMemSubmonoidUnitary
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousStar R]
:
ContinuousStar ↥(unitary R)
instance
instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousStar R]
:
ContinuousInv ↥(unitary R)
instance
instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousMul R]
[ContinuousStar R]
: