Structures · Analysis
NonUnitalCStarAlgebra
The class of non-unital (complex) C⋆-algebras.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Classes
- Shape
- One type argument
Extends8
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances7
- BoundedContinuousFunction
- CStarMatrix
- ZeroAtInftyContinuousMap
- Subtype
- Prod
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by229
- CStarMatrix.toCLM
- PositiveLinearMap.PreGNS
- PositiveLinearMap.ofPreGNS
- Unitization.inr_le_iff
- Unitization.inr_nonneg_iff
- CStarAlgebra.norm_le_norm_of_nonneg_of_le
- PositiveLinearMap.toPreGNS
- CStarModule.norm_sq_eq
- PositiveLinearMap.leftMulMapPreGNS
- IsStarProjection.le_tfae
- CStarModule.innerSL
- IsStarNormal.norm_add_eq_max
- CFC.monotone_nnrpow
- CStarModule.normedAddCommGroup
- Unitization.cfcₙ_eq_cfc_inr
- CStarModule.norm_nonneg
- PositiveLinearMap.GNS
- PositiveLinearMap.gnsNonUnitalStarAlgHom
- NonUnitalStarAlgHom.norm_map
- CStarMatrix.toCLM_apply_single_apply
- CStarAlgebra.spectralOrder
- CStarMatrix.toCLM_apply_single
- IsStarNormal.commute_star_right
- CStarAlgebra.isBasis_nonneg_sections
- WithCStarModule.pi_norm_sq
- Filter.IsIncreasingApproximateUnit.eventually_norm
- CFC.monotoneOn_one_sub_one_add_inv
- CStarMatrix.toCLMNonUnitalAlgHom
- WithCStarModule.norm_apply_le_norm
- IsSelfAdjoint.norm_add_eq_max
- CFC.concaveOn_nnrpow
- CStarAlgebra.span_nonneg_inter_closedBall
- PositiveLinearMap.leftMulMapPreGNS_apply
- CStarAlgebra.approximateUnit
- CStarModule.norm_inner_le
- NonUnitalStarAlgHom.nnnorm_apply_le
- SemiconjBy.star_right
- CStarMatrix.ofMatrixL
- Unitization.LE.le.of_inr
- CStarAlgebra.inr_mem_Icc_iff_norm_le
- CStarModule.normedSpaceCore
- CStarAlgebra.exists_sum_four_nonneg
- CStarModule.norm_zero_iff
- IsStarProjection.le_iff_mul_eq_right
- WithCStarModule.pi_norm
- isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
- IsStarNormal.commute_star_left
- CStarAlgebra.spectralOrderedRing
- CStarAlgebra.star_right_conjugate_le_norm_smul
- CStarModule.norm_pos
Ancestors100
- 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
- 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
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedRing
- NonUnitalRing
- 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