Basic

📁 Source: Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

Statistics

Metric	Count
Definitions spectralOrder, characterSpaceHomeo, characterSpaceToSpectrum, instCommCStarAlgebraSubtypeMemStarSubalgebraComplexOfIsStarNormal, instNormedCommRingSubtypeMemStarSubalgebraOfIsStarNormal, continuousFunctionalCalculus	6
Theorems instNonnegSpectrumClass, instNonnegSpectrumClass', instNonnegSpectrumClassComplexUnital, spectralOrderedRing, coe_mem_spectrum_complex, instIsometricContinuousFunctionalCalculus, instNonUnitalIsometricContinuousFunctionalCalculus, sq_spectrumRestricts, instContinuousFunctionalCalculus, instIsometricContinuousFunctionalCalculus, instNonUnitalContinuousFunctionalCalculus, instNonUnitalIsometricContinuousFunctionalCalculus, eq_zero_of_neg, nnreal_add, nnreal_iff_nnnorm, smul_of_nonneg, bijective_characterSpaceToSpectrum, characterSpaceToSpectrum_coe, continuous_characterSpaceToSpectrum, cfcₙ_eq_cfc_inr, complex_cfcₙ_eq_cfc_inr, real_cfcₙ_eq_cfc_inr, cfcHom_eq_of_isStarNormal, continuousFunctionalCalculus_map_id, inr_comp_cfcₙHom_eq_cfcₙAux, spectrum_star_mul_self_nonneg	26
Total	32

CStarAlgebra

Definitions

Name	Category	Theorems
spectralOrder 📖	CompOp	1 math math: spectralOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonnegSpectrumClass 📖	mathematical	—	NonnegSpectrumClass Real Real.instCommSemiring Real.partialOrder NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing toNonUnitalCStarAlgebra NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace	—	NonnegSpectrumClass.of_spectrum_nonneg AddSubmonoid.closure_induction spectrum_star_mul_self_nonneg Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim spectrum.of_subsingleton instIsEmptyFalse spectrum.zero_eq SpectrumRestricts.nnreal_iff SpectrumRestricts.nnreal_add IsSelfAdjoint.of_nonneg StarOrderedRing.nonneg_iff
instNonnegSpectrumClass' 📖	mathematical	—	NonnegSpectrumClass Real Real.instCommSemiring Real.partialOrder NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace	—	NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal IsScalarTower.left Unitization.quasispectrum_eq_spectrum_inr' spectralOrderedRing spectrum_nonneg_of_nonneg instNonnegSpectrumClass NonUnitalCStarAlgebra.toStarModule StarOrderedRing.nonneg_iff DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass AddSubmonoid.mem_map_of_mem AddSubmonoid.closure_mono Unitization.inr_mul Unitization.inr_star Set.range_comp AddMonoidHom.map_mclosure
instNonnegSpectrumClassComplexUnital 📖	mathematical	—	NonnegSpectrumClass Complex Complex.instCommSemiring Complex.partialOrder NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing toNonUnitalCStarAlgebra NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNormedSpace	—	mem_quasispectrum_iff ge_of_eq SpectrumRestricts.algebraMap_image IsScalarTower.complexToReal IsScalarTower.left IsSelfAdjoint.spectrumRestricts IsStarNormal.instContinuousFunctionalCalculus IsSelfAdjoint.of_nonneg spectrum_nonneg_of_nonneg instNonnegSpectrumClass
spectralOrderedRing 📖	mathematical	—	StarOrderedRing NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing spectralOrder NonUnitalCStarAlgebra.toStarRing	—	CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus AddSubmonoid.subset_closure IsSelfAdjoint.star_eq eq_sub_iff_add_eq' add_sub_cancel_left AddSubmonoid.closure_induction IsSelfAdjoint.star_mul_self NNReal.instIsScalarTowerOfReal IsScalarTower.left quasispectrumRestricts_iff_spectrumRestricts_inr' SpectrumRestricts.nnreal_iff Unitization.inr_mul Unitization.inr_star spectrum_star_mul_self_nonneg spectrum.zero_eq Unitization.instNontrivialLeft Complex.instNontrivial AddTorsor.nonempty Unitization.isSelfAdjoint_inr Unitization.inr_add IsSelfAdjoint.add SpectrumRestricts.nnreal_add

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mem_spectrum_complex 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	Complex Set Set.instMembership spectrum Complex.instCommSemiring Complex.ofReal Real Real.instCommSemiring Algebra.complexToReal Ring.toSemiring	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar SpectrumRestricts.algebraMap_image IsScalarTower.complexToReal IsScalarTower.left spectrumRestricts Set.image_congr
instIsometricContinuousFunctionalCalculus 📖	mathematical	—	IsometricContinuousFunctionalCalculus Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing Real.instCommSemiring instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal NormedRing.toMetricSpace NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra	—	SpectrumRestricts.isometric_cfc IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsStarNormal.instIsometricContinuousFunctionalCalculus Real.instCompleteSpace Real.instContinuousMapUniqueHom TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Complex.isometry_ofReal zero isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts IsScalarTower.right Algebra.to_smulCommClass IsStarNormal.instNonUnitalContinuousFunctionalCalculus
instNonUnitalIsometricContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalIsometricContinuousFunctionalCalculus Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing 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 NonUnitalNormedRing.toMetricSpace NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace IsScalarTower.complexToReal NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup Complex Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalCStarAlgebra.toIsScalarTower SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass	—	QuasispectrumRestricts.isometric_cfc IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus Real.instCompleteSpace RCLike.uniqueNonUnitalContinuousFunctionalCalculus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Complex.isometry_ofReal zero isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts IsStarNormal.instNonUnitalContinuousFunctionalCalculus
sq_spectrumRestricts 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing	SpectrumRestricts NNReal Real NNReal.instSemifield Field.toSemifield Real.instField NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id Real.instCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal	—	SpectrumRestricts.nnreal_iff IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus cfc_id cfc_pow continuousOn_id' cfc_map_spectrum Continuous.comp_continuousOn' Continuous.pow IsTopologicalSemiring.toContinuousMul continuous_id' sq_nonneg StarOrderedRing.toExistsAddOfLE Real.instStarOrderedRing IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid

IsStarNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousFunctionalCalculus 📖	mathematical	—	ContinuousFunctionalCalculus Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CStarAlgebra.toStarRing Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra CStarAlgebra.toNormedAlgebra	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar zero spectrum.instCompactSpace CStarAlgebra.toCompleteSpace Complex.instProperSpace spectrum.nonempty CStarAlgebra.toStarModule NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing StarSubalgebra.subsemiringClass StarSubalgebra.starMemClass IsTopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toContinuousMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup AlgEquivClass.toAlgHomClass instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarRingHomClass.toStarHomClass RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass Isometry.isClosedEmbedding ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace Complex.instCompleteSpace CompactlyCoherentSpace.of_sequentialSpace FrechetUrysohnSpace.to_sequentialSpace Subtype.instFrechetUrysohnSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Isometry.comp isometry_subtype_coe StarAlgEquiv.isometry NonUnitalAlgHomClass.toNonUnitalRingHomClass instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass StarAlgebra.elemental.self_mem continuousFunctionalCalculus_map_id StarSubalgebra.subringClass StarSubalgebra.spectrum_eq StarAlgebra.elemental.isClosed AlgEquiv.spectrum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ContinuousMap.spectrum_eq_range StarHomClass.map_star StarAlgHom.instStarHomClass Commute.map NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass Commute.all
instIsometricContinuousFunctionalCalculus 📖	mathematical	—	IsometricContinuousFunctionalCalculus Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CStarAlgebra.toStarRing Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NormedRing.toMetricSpace NormedAlgebra.toAlgebra NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instContinuousFunctionalCalculus ContinuousFunctionalCalculus.compactSpace_spectrum CStarAlgebra.toStarModule NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing StarSubalgebra.subsemiringClass StarSubalgebra.starMemClass IsTopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toContinuousMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup AlgEquivClass.toAlgHomClass instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarRingHomClass.toStarHomClass RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass cfcHom_eq_of_isStarNormal Isometry.comp isometry_subtype_coe StarAlgEquiv.isometry spectrum.instCompactSpace CStarAlgebra.toCompleteSpace Complex.instProperSpace NonUnitalAlgHomClass.toNonUnitalRingHomClass instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass
instNonUnitalContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalContinuousFunctionalCalculus Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass	—	RCLike.nonUnitalContinuousFunctionalCalculus NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass NonUnitalCStarAlgebra.toStarModule Unitization.isStarNormal_inr instContinuousFunctionalCalculus NonUnitalCStarAlgebra.toCompleteSpace NonUnitalCStarAlgebra.toCStarRing
instNonUnitalIsometricContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalIsometricContinuousFunctionalCalculus Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalNormedRing.toMetricSpace NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNormedSpace NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass instNonUnitalContinuousFunctionalCalculus AddMonoidHomClass.isometry_of_norm IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul quasispectrum.instCompactSpace NonUnitalCStarAlgebra.toCompleteSpace Complex.instProperSpace DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass NonUnitalStarAlgHom.instNonUnitalAlgHomClass CStarRing.instRegularNormedAlgebra NonUnitalCStarAlgebra.toCStarRing Unitization.norm_inr Unitization.inrNonUnitalStarAlgHom_apply NonUnitalStarAlgHom.comp_apply NonUnitalCStarAlgebra.toStarModule Unitization.isStarNormal_inr instContinuousFunctionalCalculus inr_comp_cfcₙHom_eq_cfcₙAux RCLike.instContinuousStar IsLocalRing.toNontrivial Field.instIsLocalRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup cfcₙAux.eq_1 ContinuousFunctionalCalculus.compactSpace_spectrum IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus instIsometricContinuousFunctionalCalculus Unitization.instIsStarNormal norm_cfcHom spectrum.instCompactSpace Unitization.instCompleteSpace Complex.instCompleteSpace StarAlgEquiv.norm_map StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarRingHomClass.toStarHomClass NonUnitalAlgHomClass.toNonUnitalRingHomClass instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass

SpectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_neg 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing SpectrumRestricts NNReal Real NNReal.instSemifield Field.toSemifield Real.instField NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id Real.instCommSemiring DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	CFC.eq_zero_of_spectrum_subset_zero IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus Set.subset_singleton_iff Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le nnreal_iff neg_neg
nnreal_add 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing SpectrumRestricts NNReal Real NNReal.instSemifield Field.toSemifield Real.instField NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id Real.instCommSemiring DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	nnreal_iff_nnnorm IsSelfAdjoint.add nnnorm_add_le NNReal.coe_add map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass add_sub_add_comm LE.le.trans add_le_add NNReal.addLeftMono covariant_swap_add_of_covariant_add le_refl
nnreal_iff_nnnorm 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra	SpectrumRestricts Real NNReal.instSemifield Field.toSemifield Real.instField NNReal.instAlgebraOfReal Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id Real.instCommSemiring DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap NNReal.toReal	—	IsSelfAdjoint.sub IsSelfAdjoint.algebraMap StarModule.complexToReal CStarAlgebra.toStarModule IsSelfAdjoint.all instTrivialStarReal ENNReal.coe_le_coe IsSelfAdjoint.spectralRadius_eq_nnnorm spectralRadius_eq IsScalarTower.complexToReal IsScalarTower.left IsSelfAdjoint.spectrumRestricts IsStarNormal.instContinuousFunctionalCalculus nnreal_iff_spectralRadius_le
smul_of_nonneg 📖	mathematical	SpectrumRestricts NNReal Real NNReal.instSemifield Field.toSemifield Real.instField NNReal.instAlgebraOfReal Ring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id Real.instCommSemiring DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal Real.instLE Real.instZero	Algebra.toSMul	—	nnreal_iff Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim spectrum.of_subsingleton instIsEmptyFalse Eq.le zero_smul spectrum.zero_eq CanLift.prf instCanLiftUnitsValIsUnit le_of_smul_le_smul_left PosSMulReflectLT.toPosSMulReflectLE Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors PosSMulMono.toPosSMulReflectLT IsOrderedModule.toPosSMulMono instIsOrderedModule Real.instStarOrderedRing RCLike.instStarModuleReal IsScalarTower.right Algebra.to_smulCommClass MulZeroClass.mul_zero Units.val_inv_eq_inv_val Set.mem_smul_set_iff_inv_smul_mem spectrum.unit_smul_eq_smul Units.smul_def inv_pos RCLike.toPosMulReflectLT lt_of_le_of_ne

StarAlgebra.elemental

Definitions

Name	Category	Theorems
characterSpaceHomeo 📖	CompOp	—
characterSpaceToSpectrum 📖	CompOp	3 math math: characterSpaceToSpectrum_coe, bijective_characterSpaceToSpectrum, continuous_characterSpaceToSpectrum
instCommCStarAlgebraSubtypeMemStarSubalgebraComplexOfIsStarNormal 📖	CompOp	2 math math: cfcHom_eq_of_isStarNormal, continuousFunctionalCalculus_map_id
instNormedCommRingSubtypeMemStarSubalgebraOfIsStarNormal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_characterSpaceToSpectrum 📖	mathematical	—	Function.Bijective Set.Elem WeakDual Complex StarSubalgebra Complex.instCommSemiring Complex.instStarRing Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra CStarAlgebra.toStarModule SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Algebra.id Ring.uniformContinuousConstSMul Complex.instRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocSemiring.toAddCommMonoid SubringClass.toNormedRing StarSubalgebra.subringClass Complex.commRing NormedSpace.toModule instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental NonUnitalCStarAlgebra.toNormedSpace instTopologicalSpaceSubtype WeakDual.characterSpace spectrum characterSpaceToSpectrum	—	CStarAlgebra.toStarModule IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul StarSubalgebra.subringClass starAlgHomClass_ext Complex.instT2Space WeakDual.CharacterSpace.instAlgHomClass NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace WeakDual.CharacterSpace.instStarHomClass ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass WeakDual.CharacterSpace.instContinuousLinearMapClass self_mem StarSubalgebra.spectrum_eq isClosed WeakDual.CharacterSpace.mem_spectrum_iff_exists instCompleteSpaceSubtypeMemStarSubalgebra CStarAlgebra.toCompleteSpace
characterSpaceToSpectrum_coe 📖	mathematical	—	Complex Set Set.instMembership spectrum Complex.instCommSemiring NormedRing.toRing CStarAlgebra.toNormedRing NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra characterSpaceToSpectrum DFunLike.coe Set.Elem WeakDual StarSubalgebra Complex.instStarRing Ring.toSemiring CStarAlgebra.toStarRing CStarAlgebra.toStarModule SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubringClass.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental NonUnitalCStarAlgebra.toNormedSpace instTopologicalSpaceSubtype WeakDual.characterSpace WeakDual.CharacterSpace.instFunLike	—	CStarAlgebra.toStarModule IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul StarSubalgebra.subringClass
continuous_characterSpaceToSpectrum 📖	mathematical	—	Continuous Set.Elem WeakDual Complex StarSubalgebra Complex.instCommSemiring Complex.instStarRing Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra CStarAlgebra.toStarModule SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Algebra.id Ring.uniformContinuousConstSMul Complex.instRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocSemiring.toAddCommMonoid SubringClass.toNormedRing StarSubalgebra.subringClass Complex.commRing NormedSpace.toModule instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental NonUnitalCStarAlgebra.toNormedSpace instTopologicalSpaceSubtype WeakDual.characterSpace spectrum Set Set.instMembership instTopologicalSpaceWeakDual characterSpaceToSpectrum	—	CStarAlgebra.toStarModule IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul StarSubalgebra.subringClass continuous_induced_rng ContinuousMapClass.map_continuous SMulCommClass.continuousConstSMul Algebra.to_smulCommClass ContinuousMap.instContinuousMapClass NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass self_mem

Unitization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcₙ_eq_cfc_inr 📖	mathematical	inr Complex Complex.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	cfcₙ Semifield.toCommSemiring IsDomain.toNontrivial instIsDomain NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NonUnitalCStarAlgebra.toStarRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing cfc Unitization instUniformSpace DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField instRing Complex.commRing NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass instStarRing Complex.instCommSemiring Complex.instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalCStarAlgebra.toStarModule instAlgebra NonUnitalRing.toNonUnitalSemiring Module.toDistribMulAction CommSemiring.toSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup	—	IsDomain.toNontrivial instIsDomain NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass NonUnitalCStarAlgebra.toStarModule IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital cfcₙ_eq_cfc quasispectrum_inr_eq NonUnitalStarAlgHom.map_cfcₙ instIsScalarTower ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass NonUnitalStarAlgHom.instContinuousLinearMapClassComplex NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass not_and_or cfcₙ_apply_of_not_continuousOn inr_zero cfc_apply_of_not_continuousOn quasispectrum_eq_spectrum_inr' cfcₙ_apply_of_not_predicate cfc_apply_of_not_predicate not_iff_not
complex_cfcₙ_eq_cfc_inr 📖	mathematical	Complex Complex.instZero	inr cfcₙ IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass IsStarNormal.instNonUnitalContinuousFunctionalCalculus cfc Unitization NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing instCStarAlgebra CStarAlgebra.toStarRing instUniformSpace DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField instRing Complex.commRing instStarRing NonUnitalCStarAlgebra.toStarModule instAlgebra NonUnitalRing.toNonUnitalSemiring Algebra.id Module.toDistribMulAction CommSemiring.toSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring DistribMulAction.toMulAction IsStarNormal.instContinuousFunctionalCalculus	—	cfcₙ_eq_cfc_inr IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass Complex.instCompleteSpace IsStarNormal.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus RCLike.uniqueNonUnitalContinuousFunctionalCalculus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CStarRing.instRegularNormedAlgebra NonUnitalCStarAlgebra.toCStarRing NonUnitalCStarAlgebra.toStarModule IsScalarTower.right Algebra.to_smulCommClass isStarNormal_inr
real_cfcₙ_eq_cfc_inr 📖	mathematical	Real Real.instZero	inr Complex Complex.instZero cfcₙ IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing StarRing.toStarAddMonoid NonUnitalCStarAlgebra.toStarRing 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 NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace IsScalarTower.complexToReal NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup Complex.instNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalCStarAlgebra.toIsScalarTower SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus cfc Unitization NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRing Complex.commRing instStarRing Complex.instCommSemiring Complex.instStarRing NonUnitalCStarAlgebra.toStarModule instUniformSpace DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField instAlgebra NonUnitalRing.toNonUnitalSemiring NormedAlgebra.toAlgebra SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex RCLike.toNormedAlgebra Complex.instRCLike Module.toDistribMulAction CommSemiring.toSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.addCommGroup Complex.instModuleSelf NonUnitalSemiring.toNonUnitalNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.left Complex.instSemiring DistribMulAction.toMulAction IsSelfAdjoint.instContinuousFunctionalCalculus Algebra.id IsStarNormal.instContinuousFunctionalCalculus instCStarAlgebra	—	cfcₙ_eq_cfc_inr IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal NonUnitalCStarAlgebra.toIsScalarTower SMulCommClass.complexToReal NonUnitalCStarAlgebra.toSMulCommClass Real.instCompleteSpace IsScalarTower.left IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus IsSelfAdjoint.instContinuousFunctionalCalculus NonUnitalCStarAlgebra.toStarModule IsStarNormal.instContinuousFunctionalCalculus RCLike.uniqueNonUnitalContinuousFunctionalCalculus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CStarRing.instRegularNormedAlgebra NonUnitalCStarAlgebra.toCStarRing IsScalarTower.right Algebra.to_smulCommClass isSelfAdjoint_inr

(root)

Definitions

Name	Category	Theorems
continuousFunctionalCalculus 📖	CompOp	2 math math: cfcHom_eq_of_isStarNormal, continuousFunctionalCalculus_map_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcHom_eq_of_isStarNormal 📖	mathematical	—	cfcHom Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CStarAlgebra.toStarRing Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra CStarAlgebra.toNormedAlgebra IsStarNormal.instContinuousFunctionalCalculus StarAlgHom.comp ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership StarSubalgebra Ring.toSemiring CStarAlgebra.toStarModule SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SubsemiringClass.toSemiring StarSubalgebra.subsemiringClass StarSubalgebra.algebra StarMemClass.instStar StarSubalgebra.starMemClass StarSubalgebra.subtype StarAlgHomClass.toStarAlgHom StarAlgEquiv SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing ContinuousMap.instAdd Complex.instAdd IsTopologicalSemiring.toContinuousAdd Distrib.toAdd StarAlgebra.elemental.instCommCStarAlgebraSubtypeMemStarSubalgebraComplexOfIsStarNormal ContinuousMap.instMul Complex.instMul IsTopologicalSemiring.toContinuousMul ContinuousMap.instSMul Algebra.toSMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul Complex.instRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing StarAlgEquiv.instFunLike AlgEquivClass.toAlgHomClass StarAlgEquiv.instEquivLike instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarRingHomClass.toStarHomClass ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass continuousFunctionalCalculus	—	cfcHom_eq_of_continuous_of_map_id IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus Complex.instContinuousMapUniqueHom TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CStarAlgebra.toStarModule NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing StarSubalgebra.subsemiringClass StarSubalgebra.starMemClass IsTopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toContinuousMul UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup AlgEquivClass.toAlgHomClass instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarRingHomClass.toStarHomClass RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass Continuous.comp continuous_subtype_val Isometry.continuous spectrum.instCompactSpace CStarAlgebra.toCompleteSpace Complex.instProperSpace StarAlgEquiv.isometry NonUnitalAlgHomClass.toNonUnitalRingHomClass instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass StarAlgebra.elemental.self_mem continuousFunctionalCalculus_map_id
continuousFunctionalCalculus_map_id 📖	mathematical	—	DFunLike.coe StarAlgEquiv Complex ContinuousMap Set.Elem spectrum Complex.instCommSemiring NormedRing.toRing CStarAlgebra.toNormedRing NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex StarSubalgebra Complex.instStarRing Ring.toSemiring CStarAlgebra.toStarRing CStarAlgebra.toStarModule SetLike.instMembership StarSubalgebra.setLike StarAlgebra.elemental IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing ContinuousMap.instAdd Complex.instAdd IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib StarAlgebra.elemental.instCommCStarAlgebraSubtypeMemStarSubalgebraComplexOfIsStarNormal ContinuousMap.instMul Complex.instMul IsTopologicalSemiring.toContinuousMul Distrib.toMul ContinuousMap.instSMul Algebra.toSMul CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul Complex.instRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing SubsemiringClass.toSemiring StarSubalgebra.subsemiringClass StarSubalgebra.algebra ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Complex.instContinuousStar StarMemClass.instStar StarSubalgebra.starMemClass StarAlgEquiv.instFunLike continuousFunctionalCalculus ContinuousMap.restrict ContinuousMap.id StarAlgebra.elemental.self_mem	—	StarAlgEquiv.symm_apply_apply CStarAlgebra.toStarModule IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Complex.instContinuousStar
inr_comp_cfcₙHom_eq_cfcₙAux 📖	mathematical	—	NonUnitalStarAlgHom.comp Complex ContinuousMapZero Set.Elem quasispectrum Complex.instCommSemiring NonUnitalNormedRing.toNonUnitalRing NonUnitalCStarAlgebra.toNonUnitalNormedRing NormedSpace.toModule Complex.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNormedSpace quasispectrum.instZero Complex.instNontrivial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace Unitization MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring ContinuousMapZero.instNonUnitalCommSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsTopologicalSemiring.toContinuousAdd ContinuousMapZero.instModule Semiring.toModule SMulCommClass.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid ContinuousMapZero.instStarRing Complex.instStarRing Complex.instContinuousStar NonUnitalRing.toNonUnitalSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalCStarAlgebra.toStarRing Unitization.instNonAssocSemiring Unitization.instDistribMulAction Unitization.instStar AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Unitization.inrNonUnitalStarAlgHom cfcₙHom IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass IsStarNormal.instNonUnitalContinuousFunctionalCalculus cfcₙAux Complex.instRCLike NonUnitalCStarAlgebra.toStarModule Unitization.instMul Complex.instSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup SMulWithZero.toSMulZeroClass MulActionWithZero.toSMulWithZero Module.toMulActionWithZero Unitization.isStarNormal_inr IsStarNormal.instContinuousFunctionalCalculus Unitization.instCStarAlgebra	—	Unitization.isStarNormal_inr ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NonUnitalCStarAlgebra.toStarModule IsScalarTower.right NonUnitalCStarAlgebra.toIsScalarTower NonUnitalCStarAlgebra.toSMulCommClass IsScalarTower.left Algebra.to_smulCommClass RCLike.uniqueNonUnitalContinuousFunctionalCalculus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CStarRing.instRegularNormedAlgebra NonUnitalCStarAlgebra.toCStarRing quasispectrum.instCompactSpace NonUnitalCStarAlgebra.toCompleteSpace Complex.instProperSpace instFactMemSetQuasispectrumOfNat Complex.instNontrivial IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul IsStarNormal.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus Continuous.comp' Unitization.continuous_inr cfcₙHom_continuous Topology.IsClosedEmbedding.continuous IsLocalRing.toNontrivial Field.instIsLocalRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup RCLike.instContinuousStar isClosedEmbedding_cfcₙAux cfcₙHom_id cfcₙAux_id
spectrum_star_mul_self_nonneg 📖	mathematical	Real Set Set.instMembership spectrum Real.instCommSemiring NormedRing.toRing CStarAlgebra.toNormedRing NormedAlgebra.toAlgebra Real.normedField NormedRing.toSeminormedRing NormedAlgebra.complexToReal CStarAlgebra.toNormedAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CStarAlgebra.toStarRing	Real.instLE Real.instZero	—	Algebra.to_smulCommClass IsScalarTower.right IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus IsStarNormal.instNonUnitalContinuousFunctionalCalculus Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal StarMul.star_mul IsSelfAdjoint.star_eq IsSelfAdjoint.cfcₙ mul_assoc neg_mul CFC.posPart_sub_negPart mul_sub CFC.negPart_mul_posPart neg_zero sub_neg_eq_add zero_add pow_succ pow_zero one_mul IsSelfAdjoint.instContinuousFunctionalCalculus IsStarNormal.instContinuousFunctionalCalculus IsDomain.toNontrivial instIsDomain ContinuousFunctionalCalculus.toNonUnital Real.instCompleteSpace cfcₙ_eq_cfc RCLike.uniqueNonUnitalContinuousFunctionalCalculus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.continuousOn continuous_negPart instHasSolidNormReal Real.instIsOrderedAddMonoid negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono cfc_pow cfc_map_spectrum Continuous.comp_continuousOn' Continuous.pow IsTopologicalSemiring.toContinuousMul continuous_id' pow_nonneg IsOrderedRing.toZeroLEOneClass Real.instIsOrderedRing IsOrderedRing.toPosMulMono negPart_nonneg instTrivialStarReal StarModule.complexToReal CStarAlgebra.toStarModule eq_sub_iff_add_eq' star_mul_self_add_self_mul_star sub_eq_add_neg sq SpectrumRestricts.nnreal_add IsSelfAdjoint.smul StarAddMonoid.toStarModuleNat TrivialStar.star_trivial Nat.instTrivialStar IsSelfAdjoint.add IsSelfAdjoint.pow Subtype.prop IsSelfAdjoint.neg IsSelfAdjoint.star_mul_self Nat.cast_smul_eq_nsmul SpectrumRestricts.smul_of_nonneg IsSelfAdjoint.sq_spectrumRestricts Nat.instAtLeastTwoHAddOfNat eqOn_of_cfc_eq_cfc cfc_zero CFC.negPart_def SpectrumRestricts.eq_zero_of_neg SpectrumRestricts.mul_comm continuous_zero negPart_eq_zero eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass

---

← Back to Index