Structures · Analysis
NonUnitalCommCStarAlgebra
The class of non-unital commutative (complex) C⋆-algebras.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Classes
- Shape
- One type argument
Extends2
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances6
- BoundedContinuousFunction
- ZeroAtInftyContinuousMap
- Subtype
- Prod
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- NonUnitalCommCStarAlgebra.toNormedSpace
- CommCStarAlgebra.norm_add_eq_max
- NonUnitalCommCStarAlgebra.toStarRing
- CommCStarAlgebra.nnnorm_add_eq_max
- CommCStarAlgebra.norm_sub_eq_max
- instNonUnitalCommCStarAlgebraProd
- CommCStarAlgebra.nnnorm_sub_eq_max
- NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing
- instNonUnitalCommCStarAlgebraForall
- MulOpposite.instNonUnitalCommCStarAlgebra
- NonUnitalCommCStarAlgebra.toStarModule
- ZeroAtInftyContinuousMap.instNonUnitalCommCStarAlgebra
- ContinuousMap.instNonUnitalCommCStarAlgebra
- CommCStarAlgebra.nnnorm_sum_eq_sup
- NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra
- NonUnitalCommCStarAlgebra.toIsScalarTower
- Unitization.instCommCStarAlgebra
- NonUnitalCommCStarAlgebra.toCompleteSpace
- BoundedContinuousFunction.instNonUnitalCommCStarAlgebra
- NonUnitalCommCStarAlgebra.toSMulCommClass
- NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra
- NonUnitalCommCStarAlgebra.toCStarRing
- instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal
Ancestors109
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- AlgebraicGeometry.QuasiSeparated
- Bornology
- Bracket
- CStarRing
- ChartedSpace
- CommMagma
- CommSemigroup
- CompactSpace
- CompactlyCoherentSpace
- CompleteSpace
- Dist
- Distrib
- DistribMulAction
- Dvd
- EDist
- EMetricSpace
- ENorm
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- InvolutiveNeg
- InvolutiveStar
- IsLeftCancelAdd
- IsRightCancelAdd
- IsScalarTower
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- LocallyPathConnectedSpace
- MetricSpace
- Module
- Mul
- MulAction
- MulZeroClass
- NNDist
- NNNorm
- NSMul
- Neg
- NegZeroClass
- NonUnitalCStarAlgebra
- NonUnitalCommRing
- NonUnitalCommSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedCommRing
- NonUnitalNormedRing
- NonUnitalRing
- NonUnitalSeminormedCommRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Norm
- NormedAddCommGroup
- NormedAddGroup
- NormedSpace
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- SMul
- SMulCommClass
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SequentialSpace
- Star
- StarModule
- StarMul
- StarRing
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero