Structures · Analysis
CStarAlgebra
The class of unital (complex) C⋆-algebras.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Classes
- Shape
- One type argument
Extends6
Extended by1
Forgetful instances
Every CStarAlgebra is also a
Concrete types that are instances9
- ContinuousLinearMap
- BoundedContinuousFunction
- CStarMatrix
- Unitization
- DoubleCentralizer
- Subtype
- Prod
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by159
- Unitary.argSelfAdjoint
- IsSelfAdjoint.le_algebraMap_norm_self
- IsSelfAdjoint.spectralRadius_eq_nnnorm
- selfAdjoint.unitarySelfAddISMul
- CStarAlgebra.norm_le_one_iff_of_nonneg
- CStarAlgebra.norm_le_iff_le_algebraMap
- Unitary.argSelfAdjoint_coe
- IsStrictlyPositive.of_le
- Unitary.openPartialHomeomorph
- Unitary.path
- Unitary.norm_argSelfAdjoint_le_pi
- IsSelfAdjoint.mem_spectrum_eq_re
- CStarAlgebra.inv_le_inv
- CStarAlgebra.isUnit_of_le
- StarAlgebra.elemental.characterSpaceToSpectrum
- selfAdjoint.norm_sq_expUnitary_sub_one
- CFC.tendsto_ite_cfc_rpow_sub_one_ite_log
- continuousFunctionalCalculus
- IsSelfAdjoint.toReal_spectralRadius_eq_norm
- selfAdjoint.unitarySelfAddISMul_coe
- selfAdjoint.expUnitaryPathToOne
- CStarAlgebra.mem_Icc_algebraMap_iff_norm_le
- expUnitary_argSelfAdjoint
- SpectrumRestricts.nnreal_add
- Unitary.spectrum_subset_slitPlane_iff_norm_lt_two
- SpectrumRestricts.nnreal_iff_nnnorm
- Unitary.two_mul_one_sub_le_norm_sub_one_sq
- CStarAlgebra.inv_le_inv_iff
- CStarAlgebra.inv_le_one
- Unitary.norm_sub_one_sq_eq
- Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
- CStarAlgebra.toReal_spectralRadius_star_mul_self_eq_norm_sq
- Unitary.norm_sub_eq
- IsSelfAdjoint.val_re_map_spectrum
- le_iff_norm_sqrt_mul_rpow
- CFC.conjugate_rpow_neg_one_half
- le_iff_norm_sqrt_mul_sqrt_inv
- CStarAlgebra.convexOn_ringInverse_algebraMap_add
- CFC.log_monotoneOn
- Unitary.expUnitary_eq_mul_inv
- spectrum_star_mul_self_nonneg
- CFC.concaveOn_rpow
- CStarAlgebra.exists_sum_four_unitary
- CStarAlgebra.pow_antitone
- CStarAlgebra.mem_Icc_iff_norm_le_one
- CStarAlgebra.nnnorm_mem_spectrum_of_nonneg
- CFC.rpow_le_rpow
- CStarAlgebra.rpow_neg_one_le_rpow_neg_one
- IsSelfAdjoint.im_eq_zero_of_mem_spectrum
- Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le
Ancestors124
- 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
- CStarRing
- ChartedSpace
- CompactSpace
- CompactlyCoherentSpace
- CompleteSpace
- Dist
- Distrib
- DistribMulAction
- Dvd
- EDist
- EMetricSpace
- ENorm
- HAdd
- HMul
- HSMul
- HSub
- HVAdd
- IntCast
- InvolutiveNeg
- InvolutiveStar
- IsLeftCancelAdd
- IsRightCancelAdd
- IsScalarTower
- IsSemiprimaryRing
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- 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
- NonAssocRing
- NonAssocSemiring
- NonUnitalCStarAlgebra
- NonUnitalNonAssocRing
- NonUnitalNonAssocSemiring
- NonUnitalNormedRing
- NonUnitalRing
- NonUnitalSeminormedRing
- NonUnitalSemiring
- Nonempty
- Norm
- NormedAddCommGroup
- NormedAddGroup
- NormedAlgebra
- NormedRing
- NormedSpace
- OfNat
- One
- PrespectralSpace
- PseudoEMetricSpace
- PseudoMetricSpace
- QuasiSeparatedSpace
- Ring
- SMul
- SMulCommClass
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SeminormedAddCommGroup
- SeminormedAddGroup
- SeminormedRing
- Semiring
- SequentialSpace
- Star
- StarModule
- StarMul
- StarRing
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- TopologicalSpace
- Topology.IsGeneratedBy
- UniformSpace
- VAdd
- VSub
- ZSMul
- Zero