Structures · Analysis
CommCStarAlgebra
The class of unital commutative (complex) C⋆-algebras.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Classes
- Shape
- One type argument
Extends2
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CommCStarAlgebra is also a
Concrete types that are instances7
- Complex
- BoundedContinuousFunction
- Unitization
- Subtype
- Prod
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by22
- gelfandStarTransform
- gelfandTransform_map_star
- gelfandTransform_isometry
- CommCStarAlgebra.toStarRing
- gelfandTransform_bijective
- CommCStarAlgebra.toNormedAlgebra
- CommCStarAlgebra.toStarModule
- instCommCStarAlgebraProd
- BoundedContinuousFunction.instCommCStarAlgebra
- instCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNRealOfNontrivial
- gelfandStarTransform_symm_apply
- ContinuousMap.instCommCStarAlgebra
- gelfandStarTransform_apply_apply
- CommCStarAlgebra.toCStarRing
- gelfandStarTransform_naturality
- MulOpposite.instCommCStarAlgebra
- instCommCStarAlgebraForall
- CommCStarAlgebra.toNormedCommRing
- StarSubalgebra.commCStarAlgebra
- CommCStarAlgebra.toNonUnitalCommCStarAlgebra
- CommCStarAlgebra.toCStarAlgebra
- CommCStarAlgebra.toCompleteSpace
Ancestors146
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommGroupWithOne
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- Algebra
- AlgebraicGeometry.QuasiSeparated
- Bornology
- Bracket
- CStarAlgebra
- CStarRing
- ChartedSpace
- CommMagma
- CommMonoid
- CommMonoidWithZero
- CommRing
- CommSemigroup
- CommSemiring
- CompactSpace
- CompactlyCoherentSpace
- CompleteSpace
- Dist
- Distrib
- DistribMulAction
- Dvd
- EDist
- EMetricSpace
- ENorm
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- Ideal.FiniteHeight
- IntCast
- InvolutiveNeg
- InvolutiveStar
- IsJacobsonRing
- IsLeftCancelAdd
- IsRightCancelAdd
- IsScalarTower
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.CommRing
- Lean.Grind.CommSemiring
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- Lean.Grind.Ring
- Lean.Grind.Semiring
- LocallyPathConnectedSpace
- MetricSpace
- Module
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NNDist
- NNNorm
- NPow
- NSMul
- NatCast
- Neg
- NegZeroClass
- NonAssocCommRing
- NonAssocCommSemiring
- NonAssocRing
- NonAssocSemiring
- NonUnitalCStarAlgebra
- NonUnitalCommCStarAlgebra
- NonUnitalCommRing
- NonUnitalCommSemiring
- NonUnitalNonAssocCommRing
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedCommRing
- NonUnitalNormedRing
- NonUnitalRing
- NonUnitalSeminormedCommRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Norm
- NormedAddCommGroup
- NormedAddGroup
- NormedAlgebra
- NormedCommRing
- NormedRing
- NormedSpace
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- Ring
- SMul
- SMulCommClass
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SeminormedCommRing
- SeminormedRing
- Semiring
- SequentialSpace
- Star
- StarModule
- StarMul
- StarRing
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero