instance
instContinuousMulSubtypeMemSubmonoidUnitary_leanOA
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousMul R]
:
ContinuousMul ↥(unitary R)
instance
instContinuousStarSubtypeMemSubmonoidUnitary_leanOA
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousStar R]
:
ContinuousStar ↥(unitary R)
instance
instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar_leanOA
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousStar R]
:
ContinuousInv ↥(unitary R)
instance
instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar_leanOA
{R : Type u_1}
[Monoid R]
[StarMul R]
[TopologicalSpace R]
[ContinuousMul R]
[ContinuousStar R]
: