Basic

📁 Source: Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Basic.lean

Statistics

Metric	Count
Definitions instNegPart, instPosPart	2
Theorems le_posPart, negPart_algebraMap, negPart_def, negPart_eq_neg, negPart_eq_of_eq_PosPart_sub, negPart_eq_zero_iff, negPart_eq_zero_of_not_isSelfAdjoint, negPart_mul_posPart, negPart_neg, negPart_nonneg, negPart_one, negPart_smul, negPart_smul_of_nonneg, negPart_smul_of_nonpos, negPart_zero, neg_negPart_le, posPart_algebraMap, posPart_algebraMap_nnreal, posPart_def, posPart_eq_of_eq_sub_negPart, posPart_eq_self, posPart_eq_zero_iff, posPart_eq_zero_of_not_isSelfAdjoint, posPart_mul_negPart, posPart_natCast, posPart_neg, posPart_negPart_unique, posPart_nonneg, posPart_one, posPart_smul, posPart_smul_of_nonneg, posPart_smul_of_nonpos, posPart_sub_negPart, posPart_zero, linear_combination_nonneg, span_nonneg	36
Total	38

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_posPart 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	Preorder.toLE PartialOrder.toPreorder PosPart.posPart CStarAlgebra.instPosPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_sub_negPart sub_le_self IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid negPart_nonneg
negPart_algebraMap 📖	mathematical	—	NegPart.negPart CStarAlgebra.instNegPart Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap instNegPart Real.lattice Real.instAddGroup	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace Real.instNontrivial negPart_def IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.continuousOn continuous_negPart instHasSolidNormReal Real.instIsOrderedAddMonoid negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono neg_zero cfc_algebraMap
negPart_def 📖	mathematical	—	NegPart.negPart CStarAlgebra.instNegPart cfcₙ Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal instNegPart Real.lattice Real.instAddGroup	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal
negPart_eq_neg 📖	mathematical	—	NegPart.negPart CStarAlgebra.instNegPart NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal neg_neg neg_nonpos IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid negPart_nonneg negPart_def cfcₙ_neg IsSelfAdjoint.neg IsSelfAdjoint.of_nonneg neg_nonneg cfcₙ_id cfcₙ_congr neg_eq_iff_eq_neg Real.instIsOrderedAddMonoid NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg IsScalarTower.left Unitization.quasispectrum_eq_spectrum_inr Unitization.inr_neg spectrum.neg_eq Set.mem_neg
negPart_eq_of_eq_PosPart_sub 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing PosPart.posPart CStarAlgebra.instPosPart Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.sub LE.le.isSelfAdjoint posPart_nonneg posPart_sub_negPart
negPart_eq_zero_iff 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	NegPart.negPart CStarAlgebra.instNegPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLE PartialOrder.toPreorder	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_eq_self posPart_sub_negPart
negPart_eq_zero_of_not_isSelfAdjoint 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	NegPart.negPart CStarAlgebra.instNegPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_apply_of_not_predicate
negPart_mul_posPart 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NegPart.negPart CStarAlgebra.instNegPart PosPart.posPart CStarAlgebra.instPosPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_def negPart_def cfcₙ_mul Continuous.continuousOn continuous_negPart instHasSolidNormReal Real.instIsOrderedAddMonoid negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono neg_zero continuous_posPart posPart_zero cfcₙ_zero cfcₙ_congr NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass le_total cfcₙ_apply_of_not_predicate MulZeroClass.mul_zero
negPart_neg 📖	mathematical	—	NegPart.negPart CStarAlgebra.instNegPart NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing PosPart.posPart CStarAlgebra.instPosPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal sub_eq_zero posPart_neg neg_neg sub_self
negPart_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_nonneg Real.instStarOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass negPart_nonneg
negPart_one 📖	mathematical	—	NegPart.negPart CStarAlgebra.instNegPart Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace Real.instNontrivial negPart_def IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.continuousOn continuous_negPart instHasSolidNormReal Real.instIsOrderedAddMonoid negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono neg_zero cfc_apply_one negPart_of_nonneg Real.instZeroLEOneClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
negPart_smul 📖	mathematical	—	NegPart.negPart CStarAlgebra.instNegPart NNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal smul_neg posPart_neg posPart_smul
negPart_smul_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	NegPart.negPart CStarAlgebra.instNegPart SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal neg_neg neg_smul negPart_neg posPart_smul_of_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
negPart_smul_of_nonpos 📖	mathematical	Real Real.instLE Real.instZero	NegPart.negPart CStarAlgebra.instNegPart SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Real.instNeg PosPart.posPart CStarAlgebra.instPosPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal neg_neg neg_smul negPart_neg posPart_smul_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
negPart_zero 📖	mathematical	—	NegPart.negPart CStarAlgebra.instNegPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_apply_zero
neg_negPart_le 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_sub_negPart le_add_of_nonneg_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid posPart_nonneg
posPart_algebraMap 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap instPosPart Real.lattice Real.instAddGroup	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace Real.instNontrivial posPart_def IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero cfc_algebraMap
posPart_algebraMap_nnreal 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace DFunLike.coe RingHom NNReal Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringNNReal RingHom.instFunLike algebraMap NNReal.instAlgebraOfReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace Real.instNontrivial posPart_def IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero IsScalarTower.algebraMap_apply NNReal.instIsScalarTowerOfReal IsScalarTower.left cfc_algebraMap posPart_of_nonneg
posPart_def 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart cfcₙ Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal instPosPart Real.lattice Real.instAddGroup	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal
posPart_eq_of_eq_sub_negPart 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NegPart.negPart CStarAlgebra.instNegPart Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	PosPart.posPart CStarAlgebra.instPosPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.sub LE.le.isSelfAdjoint negPart_nonneg posPart_sub_negPart
posPart_eq_self 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_nonneg cfcₙ_id IsSelfAdjoint.of_nonneg posPart_def cfcₙ_congr NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg
posPart_eq_zero_iff 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	PosPart.posPart CStarAlgebra.instPosPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLE PartialOrder.toPreorder	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal negPart_eq_neg posPart_sub_negPart neg_sub
posPart_eq_zero_of_not_isSelfAdjoint 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	PosPart.posPart CStarAlgebra.instPosPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_apply_of_not_predicate
posPart_mul_negPart 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing PosPart.posPart CStarAlgebra.instPosPart NegPart.negPart CStarAlgebra.instNegPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_def negPart_def cfcₙ_mul Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero continuous_negPart negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono neg_zero cfcₙ_zero cfcₙ_congr NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass le_total cfcₙ_apply_of_not_predicate MulZeroClass.mul_zero
posPart_natCast 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace map_natCast RingHom.instRingHomClass posPart_algebraMap_nnreal
posPart_neg 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_def negPart_def cfcₙ_comp_neg RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero neg_neg IsSelfAdjoint.neg cfcₙ_apply_of_not_predicate
posPart_negPart_unique 📖	mathematical	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Preorder.toLE PartialOrder.toPreorder	PosPart.posPart CStarAlgebra.instPosPart NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.of_nonneg IsSelfAdjoint.neg IsSelfAdjoint.sub negPart_eq_of_eq_PosPart_sub isCompact_iff_compactSpace IsCompact.union NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum quasispectrum.zero_mem IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousMapZero.nonUnitalStarAlgHom_apply_mul_eq_zero ContinuousMapZero.mul_nonUnitalStarAlgHom_apply_eq_zero IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup RCLike.instContinuousStar cfcₙHomSuperset_id mul_neg neg_zero TrivialStar.star_trivial ContinuousMapZero.instTrivialStar instTrivialStarReal cfcₙHomSuperset_continuous StarMul.star_mul NonUnitalStarAlgHom.instStarHomClass star_zero instIsUniformAddGroupReal NonUnitalAlgHomClass.instLinearMapClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass LinearMap.map_smul' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass add_zero AddHom.map_add' map_mul NonUnitalAlgSemiHomClass.toMulHomClass mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass zero_add StarAddMonoid.star_add RCLike.uniqueNonUnitalContinuousFunctionalCalculus ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id Continuous.add sub_eq_add_neg Continuous.comp' continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid continuous_subtype_val le_rfl cfcₙ_id cfcₙ_zero cfcₙ_congr CanLift.prf Subtype.canLift Function.Injective.extend_apply Subtype.val_injective NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsScalarTower.left Unitization.quasispectrum_eq_spectrum_inr Set.mem_neg spectrum.neg_eq Unitization.inr_neg cfcₙHom_eq_cfcₙ_extend
posPart_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing PosPart.posPart CStarAlgebra.instPosPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_nonneg Real.instStarOrderedRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass posPart_nonneg
posPart_one 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart Ring.toNonUnitalRing Algebra.toModule Real Real.instCommSemiring Ring.toSemiring Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Real.instCompleteSpace AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Algebra.to_smulCommClass IsScalarTower.right ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace Real.instNontrivial posPart_def IsDomain.toNontrivial instIsDomain cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero cfc_apply_one posPart_of_nonneg Real.instZeroLEOneClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
posPart_smul 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart NNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_comp_smul RCLike.uniqueNonUnitalContinuousFunctionalCalculus UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower IsScalarTower.right Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero cfcₙ_smul cfcₙ_congr mul_max_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing MulZeroClass.mul_zero eq_or_ne zero_smul posPart_zero not_iff_not IsSelfAdjoint.smul_iff instStarModuleNNRealOfReal IsSelfAdjoint.all instTrivialStarNNReal Ne.isUnit cfcₙ_apply_of_not_predicate smul_zero
posPart_smul_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	PosPart.posPart CStarAlgebra.instPosPart SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_smul
posPart_smul_of_nonpos 📖	mathematical	Real Real.instLE Real.instZero	PosPart.posPart CStarAlgebra.instPosPart SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Real.instNeg NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal neg_neg neg_smul smul_neg posPart_smul_of_nonneg neg_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid posPart_neg
posPart_sub_negPart 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup PosPart.posPart CStarAlgebra.instPosPart NegPart.negPart CStarAlgebra.instNegPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal posPart_def negPart_def cfcₙ_sub Continuous.continuousOn continuous_posPart instHasSolidNormReal Real.instIsOrderedAddMonoid posPart_zero continuous_negPart negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono neg_zero cfcₙ_id posPart_sub_negPart
posPart_zero 📖	mathematical	—	PosPart.posPart CStarAlgebra.instPosPart MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_apply_zero

CStarAlgebra

Definitions

Name	Category	Theorems
instNegPart 📖	CompOp	27 math math: CFC.posPart_smul_of_nonpos, CFC.negPart_eq_zero_of_not_isSelfAdjoint, CFC.negPart_mul_posPart, CFC.negPart_algebraMap, CFC.negPart_smul_of_nonpos, CFC.posPart_sub_negPart, nonneg_iff_isSelfAdjoint_and_negPart_eq_zero, CFC.posPart_mul_negPart, CFC.negPart_eq_neg, CFC.negPart_nonneg, CFC.negPart_eq_zero_iff, CFC.negPart_zero, linear_combination_nonneg, IsSelfAdjoint.norm_eq_max_norm_posPart_negPart, CFC.posPart_add_negPart, CFC.negPart_one, CFC.negPart_neg, CFC.posPart_neg, CFC.negPart_eq_of_eq_PosPart_sub, norm_negPart_le, CFC.negPart_def, nonneg_TFAE, CFC.negPart_smul, CFC.negPart_smul_of_nonneg, CFC.posPart_negPart_unique, CFC.abs_sub_self, CFC.neg_negPart_le
instPosPart 📖	CompOp	28 math math: CFC.posPart_smul_of_nonpos, CFC.abs_add_self, CFC.posPart_one, CFC.posPart_natCast, CFC.negPart_mul_posPart, CFC.negPart_smul_of_nonpos, CFC.posPart_sub_negPart, CFC.posPart_zero, CFC.posPart_eq_zero_iff, CFC.posPart_mul_negPart, CFC.posPart_algebraMap_nnreal, CFC.posPart_eq_zero_of_not_isSelfAdjoint, norm_posPart_le, CFC.posPart_smul, linear_combination_nonneg, IsSelfAdjoint.norm_eq_max_norm_posPart_negPart, CFC.posPart_add_negPart, CFC.posPart_smul_of_nonneg, CFC.negPart_neg, CFC.posPart_neg, CFC.posPart_algebraMap, CFC.posPart_nonneg, CFC.posPart_def, CFC.posPart_eq_self, nonneg_TFAE, CFC.posPart_eq_of_eq_sub_negPart, CFC.posPart_negPart_unique, CFC.le_posPart

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linear_combination_nonneg 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup PosPart.posPart instPosPart Module.complexToReal SMulCommClass.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.complexToReal AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid DFunLike.coe LinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing instStarRingReal instTrivialStarReal StarModule.complexToReal LinearMap.instFunLike realPart NegPart.negPart instNegPart Complex DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction Complex.I imaginaryPart	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal SMulCommClass.complexToReal instTrivialStarReal StarModule.complexToReal CFC.posPart_sub_negPart smul_sub realPart_add_I_smul_imaginaryPart
span_nonneg 📖	mathematical	—	Submodule.span Complex Complex.instSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing setOf Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Top.top Submodule Submodule.instTop	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal SMulCommClass.complexToReal eq_top_iff instTrivialStarReal StarModule.complexToReal linear_combination_nonneg AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass sub_mem Submodule.addSubgroupClass Submodule.subset_span CFC.posPart_nonneg CFC.negPart_nonneg Submodule.smul_mem

---

← Back to Index