Structures · Analysis
CStarRing
A C⋆-ring is a normed star ring that satisfies the stronger condition ‖x‖ ^ 2 ≤ ‖x⋆ * x‖
for every x. Note that this condition actually implies equality, as is shown in
norm_star_mul_self below.
- Defined in
- Mathlib.Analysis.CStarAlgebra.Basic
- Shape
- One type argument · adds norm_mul_self_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances13
- Real
- ContinuousLinearMap
- BoundedContinuousFunction
- CStarMatrix
- Quaternion
- Unitization
- DoubleCentralizer
- ContinuousMapZero
- ZeroAtInftyContinuousMap
- Subtype
- Prod
- MulOpposite
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by75
- CStarRing.norm_star_mul_self
- Unitary.mulRight
- Unitary.mulLeft
- CStarRing.norm_of_mem_unitary
- spectrum.subset_circle_of_unitary
- CStarRing.norm_coe_unitary_mul
- CStarRing.nnnorm_star_mul_self
- CStarRing.norm_self_mul_star
- CStarRing.norm_one
- DoubleCentralizer.norm_fst_eq_snd
- CFC.norm_star_mul_mul_self_of_nonneg
- CStarRing.norm_mul_coe_unitary
- CStarRing.norm_coe_unitary
- RCLike.nonUnitalContinuousFunctionalCalculus
- IsSelfAdjoint.norm_mul_self
- inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux
- CStarRing.star_mul_self_eq_zero_iff
- IsSelfAdjoint.nnnorm_pow_two_pow
- DoubleCentralizer.norm_fst
- spectrum.norm_eq_one_of_unitary
- Unitary.spectrum_subset_circle
- CStarRing.nnnorm_self_mul_star
- IsStarProjection.norm_le
- DoubleCentralizer.norm_snd
- IsSelfAdjoint.nnnorm_mul_self
- CStarRing.norm_mul_self_le
- CFC.norm_mul_mul_star_self_of_nonneg
- Unitary.symm_mulRight_apply
- CStarRing.mul_star_self_eq_zero_iff
- Unitary.mulLeft_apply
- ZeroAtInftyContinuousMap.instCStarRing
- Unitary.mulRight_one
- Unitary.symm_mulLeft_apply
- Unitary.mulLeft_mul_apply
- ContinuousMapZero.instCStarRing
- RCLike.nonUnitalContinuousFunctionalCalculusIsClosedEmbedding
- Unitary.mulRight_apply
- lp.inftyCStarRing
- CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg
- CStarRing.star_mul_self_ne_zero_iff
- CStarRing.MulOpposite.instMulOpposite
- Unitary.mulRight_trans_mulRight
- Unitary.symm_mulRight
- CFC.norm_abs
- DoubleCentralizer.nnnorm_fst
- Unitary.mulLeft.congr_simp
- DoubleCentralizer.nnnorm_fst_eq_snd
- CStarRing.norm_star_mul_self'
- Pi.cstarRing'
- CStarRing.instNormOneClassOfNontrivial
Ancestors0
No ancestors.