Instances

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

Statistics

Metric	Count
Definitions cfcₙAux	1
Theorems exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, mul_nonneg, instContinuousFunctionalCalculus, instNonUnitalContinuousFunctionalCalculus, quasispectrumRestricts, spectrumRestricts, spectrum_nonempty, commute_iff, spectrum_nonempty, instContinuousFunctionalCalculus, instNonUnitalContinuousFunctionalCalculus, isSelfAdjoint, nonUnitalContinuousFunctionalCalculus, nonUnitalContinuousFunctionalCalculusIsClosedEmbedding, cfcHom_nnreal_eq_restrict, cfcHom_real_eq_restrict, cfc_complex_eq_real, cfc_nnreal_eq_real, cfc_real_eq_complex, cfc_real_eq_nnreal, cfcₙAux_id, cfcₙAux_injective, cfcₙAux_mem_range_inr, cfcₙHom_nnreal_eq_restrict, cfcₙHom_real_eq_restrict, cfcₙ_complex_eq_real, cfcₙ_nnreal_eq_real, cfcₙ_real_eq_complex, cfcₙ_real_eq_nnreal, commute_iff_mul_nonneg, continuous_cfcₙAux, inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux, isClosedEmbedding_cfcₙAux, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, spec_cfcₙAux	36
Total	37

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid QuasispectrumRestricts NNReal Real NNReal.instCommSemiring Real.instCommSemiring NNReal.instModuleOfReal NNReal.instAlgebraOfReal CommSemiring.toSemiring Algebra.id DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid QuasispectrumRestricts NNReal Real NNReal.instCommSemiring Real.instCommSemiring NNReal.instModuleOfReal NNReal.instAlgebraOfReal CommSemiring.toSemiring Algebra.id DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal cfcₙ_predicate cfcₙ_map_quasispectrum ContinuousOn.sqrt continuousOn_id' Real.sqrt_zero Real.sqrt_nonneg cfcₙ_mul cfcₙ_id cfcₙ_congr Real.sq_sqrt QuasispectrumRestricts.nnreal_iff

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts IsSelfAdjoint.commute_iff LE.le.isSelfAdjoint CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts mul_assoc quasispectrumRestricts_iff quasispectrum.mul_comm QuasispectrumRestricts.nnreal_of_nonneg conjugate_nonneg_of_nonneg

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousFunctionalCalculus 📖	mathematical	—	ContinuousFunctionalCalculus Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid 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 Algebra.complexToReal Ring.toSemiring	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar SpectrumRestricts.cfc instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Isometry.isClosedEmbedding Real.instCompleteSpace Complex.isometry_ofReal zero isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital
instNonUnitalContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalContinuousFunctionalCalculus 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 Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup IsScalarTower.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SMulCommClass.complexToReal	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar QuasispectrumRestricts.cfc instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Isometry.isClosedEmbedding Real.instCompleteSpace Complex.isometry_ofReal zero isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts
quasispectrumRestricts 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	QuasispectrumRestricts Real Complex Real.instCommSemiring Complex.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex RCLike.toNormedAlgebra Complex.instRCLike DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Complex.instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike Complex.reCLM	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts
spectrumRestricts 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	SpectrumRestricts Real Complex Field.toSemifield Real.instField Complex.instField Algebra.complexToReal Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex RCLike.toNormedAlgebra Complex.instRCLike DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Complex.instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike Complex.reCLM	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar quasispectrumRestricts IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital
spectrum_nonempty 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	Set.Nonempty Real spectrum Real.instCommSemiring	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal ContinuousFunctionalCalculus.spectrum_nonempty

IsStrictlyPositive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commute_iff 📖	mathematical	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal commute_iff_mul_nonneg IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital nonneg IsUnit.isStrictlyPositive IsUnit.mul isUnit

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spectrum_nonempty 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Set.Nonempty NNReal spectrum instCommSemiring	—	instIsTopologicalSemiring instContinuousStar ContinuousFunctionalCalculus.spectrum_nonempty

Nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousFunctionalCalculus 📖	mathematical	—	ContinuousFunctionalCalculus NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NNReal.instCommSemiring instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal SpectrumRestricts.cfc NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology NNReal.isClosedEmbedding_coe le_rfl nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts IsScalarTower.right Algebra.to_smulCommClass ContinuousFunctionalCalculus.toNonUnital
instNonUnitalContinuousFunctionalCalculus 📖	mathematical	—	NonUnitalContinuousFunctionalCalculus NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instCommSemiring NNReal.instNontrivial instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal QuasispectrumRestricts.cfc NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology NNReal.smulCommClass_left NNReal.isClosedEmbedding_coe le_rfl nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts

QuasispectrumRestricts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint 📖	mathematical	QuasispectrumRestricts Real Complex Real.instCommSemiring Complex.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NonUnitalRing.toNonUnitalNonAssocRing NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex RCLike.toNormedAlgebra Complex.instRCLike DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Complex.instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike Complex.reCLM	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonUnitalContinuousFunctionalCalculus 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	NonUnitalContinuousFunctionalCalculus Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar NonUnitalNormedRing.toNonUnitalRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing Unitization.inr_zero cfc_predicate_zero ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus quasispectrum.instCompactSpace FiniteDimensional.proper_real FiniteDimensional.rclike_to_real IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass NonUnitalStarSubalgebra.instStarMemClass instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass NonUnitalStarRingHomClass.toStarHomClass CStarRing.instRegularNormedAlgebra RingEquivClass.toNonUnitalRingHomClass NonUnitalAlgEquivClass.toRingEquivClass StarRingEquivClass.instNonUnitalStarRingHomClass StarAlgEquiv.instStarRingEquivClass cfcₙAux_mem_range_inr StarAlgEquiv.apply_symm_apply IsTopologicalSemiring.toIsSemitopologicalSemiring Topology.IsEmbedding.continuous_iff Isometry.isEmbedding Unitization.isometry_inr continuous_cfcₙAux Continuous.comp' Unitization.continuous_inr Continuous.snd continuous_induced_dom EquivLike.toEmbeddingLike StarRingEquiv.instRingEquivClass RingEquiv.injective Function.Injective.codRestrict cfcₙAux_injective Unitization.inr_injective cfcₙAux_id spec_cfcₙAux Unitization.quasispectrum_eq_spectrum_inr' cfcHom_predicate
nonUnitalContinuousFunctionalCalculusIsClosedEmbedding 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	NonUnitalClosedEmbeddingContinuousFunctionalCalculus Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField toDenselyNormedField IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing toStarRing NormedField.toMetricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar NonUnitalNormedRing.toNonUnitalRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instContinuousStar IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing nonUnitalContinuousFunctionalCalculus CStarRing.instRegularNormedAlgebra IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Topology.IsClosedEmbedding.of_comp_iff Isometry.isClosedEmbedding Unitization.isometry_inr IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux isClosedEmbedding_cfcₙAux

(root)

Definitions

Name	Category	Theorems
cfcₙAux 📖	CompOp	8 math math: isClosedEmbedding_cfcₙAux, inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux, cfcₙAux_id, inr_comp_cfcₙHom_eq_cfcₙAux, cfcₙAux_injective, spec_cfcₙAux, cfcₙAux_mem_range_inr, continuous_cfcₙAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfcHom_nnreal_eq_restrict 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	cfcHom NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Semifield.toCommSemiring NNReal.instSemifield instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring Nonneg.instContinuousFunctionalCalculus SpectrumRestricts.starAlgHom Real NNReal.instTopologicalSpace Field.toSemifield Real.instField instStarRingReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id Real.instCommSemiring NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid AddCommMonoid.toAddMonoid Real.instAddCommMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule Algebra.toSMul IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul Real.pseudoMetricSpace Real.instAdd SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction IsTopologicalSemiring.toIsModuleTopology IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring StarRing.toStarAddMonoid IsSelfAdjoint.of_nonneg ContinuousMap.realToNNReal SpectrumRestricts.nnreal_of_nonneg	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal SpectrumRestricts.cfcHom_eq_restrict NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Nonneg.instContinuousFunctionalCalculus NNReal.instContinuousMap.UniqueHom SpectrumRestricts.nnreal_of_nonneg IsSelfAdjoint.of_nonneg
cfcHom_real_eq_restrict 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	cfcHom Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid Semifield.toCommSemiring Field.toSemifield Real.instField instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Algebra.complexToReal Ring.toSemiring IsSelfAdjoint.instContinuousFunctionalCalculus SpectrumRestricts.starAlgHom Complex Complex.instField Complex.instStarRing MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace Complex.instNormedField NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing RCLike.toNormedAlgebra Complex.instRCLike IsScalarTower.complexToReal Complex.addCommGroup Complex.instModuleSelf Ring.toAddCommGroup Algebra.toModule Complex.instCommSemiring Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring DistribMulAction.toMulAction Module.toDistribMulAction Complex.instStarModuleReal IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace Real.instZero Complex.instZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NormedSpace.toIsBoundedSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSelfAdjoint.isStarNormal toContinuousMap ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.instAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousLinearMap.funLike ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Complex.reCLM IsSelfAdjoint.spectrumRestricts	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar SpectrumRestricts.cfcHom_eq_restrict instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsSelfAdjoint.instContinuousFunctionalCalculus Real.instContinuousMapUniqueHom ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass IsSelfAdjoint.isStarNormal IsSelfAdjoint.spectrumRestricts
cfc_complex_eq_real 📖	mathematical	Star.star Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex StarRing.toStarAddMonoid Complex.instStarRing IsSelfAdjoint NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid 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 Real IsSelfAdjoint Real.instCommSemiring instStarRingReal Real.metricSpace NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Algebra.complexToReal Ring.toSemiring IsSelfAdjoint.instContinuousFunctionalCalculus Complex.re Complex.ofReal	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.instContinuousFunctionalCalculus cfc_real_eq_complex cfc_congr SpectrumRestricts.real_iff IsSelfAdjoint.spectrumRestricts
cfc_nnreal_eq_real 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	cfc NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NNReal.instCommSemiring instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring Nonneg.instContinuousFunctionalCalculus Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid 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 NNReal.toReal Real.toNNReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal SpectrumRestricts.cfc_eq_restrict NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Nonneg.instContinuousFunctionalCalculus NNReal.instContinuousMap.UniqueHom NNReal.isClosedEmbedding_coe IsSelfAdjoint.of_nonneg SpectrumRestricts.nnreal_of_nonneg
cfc_real_eq_complex 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid	cfc Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid 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 Algebra.complexToReal Ring.toSemiring IsSelfAdjoint.instContinuousFunctionalCalculus Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.re	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar SpectrumRestricts.cfc_eq_restrict instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsSelfAdjoint.instContinuousFunctionalCalculus Real.instContinuousMapUniqueHom ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Isometry.isClosedEmbedding Real.instCompleteSpace Complex.isometry_ofReal IsSelfAdjoint.isStarNormal IsSelfAdjoint.spectrumRestricts
cfc_real_eq_nnreal 📖	mathematical	Real Real.instLE Real.instZero Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	cfc Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid 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 NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NNReal.instCommSemiring instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instAlgebraOfReal Ring.toSemiring Nonneg.instContinuousFunctionalCalculus Real.toNNReal NNReal.toReal	—	IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar Nonneg.instContinuousFunctionalCalculus cfc_nnreal_eq_real cfc_congr Real.coe_toNNReal spectrum_nonneg_of_nonneg
cfcₙAux_id 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Unitization MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousMapZero.instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMapZero.instModule NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing IsTopologicalRing.toIsTopologicalSemiring RCLike.toStarRing RCLike.instContinuousStar NonAssocRing.toNonUnitalNonAssocRing Unitization.instNonAssocRing NonUnitalRing.toNonUnitalNonAssocRing Unitization.instDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalSeminormedRing.toPseudoMetricSpace Unitization.instStar NonUnitalStarAlgHom.instFunLike cfcₙAux ContinuousMapZero.id instFactMemSetQuasispectrumOfNat Unitization.inr	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsScalarTower.left cfcHom_id
cfcₙAux_injective 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Unitization DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousMapZero.instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMapZero.instModule NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing IsTopologicalRing.toIsTopologicalSemiring RCLike.toStarRing RCLike.instContinuousStar NonAssocRing.toNonUnitalNonAssocRing Unitization.instNonAssocRing NonUnitalRing.toNonUnitalNonAssocRing Unitization.instDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalSeminormedRing.toPseudoMetricSpace Unitization.instStar NonUnitalStarAlgHom.instFunLike cfcₙAux	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing cfcHom_injective Equiv.injective Topology.IsEmbedding.injective ContinuousMapZero.instContinuousMapClass ContinuousMapZero.isEmbedding_toContinuousMap
cfcₙAux_mem_range_inr 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	Unitization NonUnitalStarSubalgebra Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonAssocSemiring.toNonUnitalNonAssocSemiring Unitization.instNonAssocSemiring CommSemiring.toSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Unitization.instModule NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toNonAssocSemiring NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedField.toNormedSpace Unitization.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing RCLike.toStarRing AddCommMonoid.toAddMonoid NonUnitalRing.toNonUnitalNonAssocRing SetLike.instMembership NonUnitalStarSubalgebra.instSetLike NonUnitalStarAlgHom.range NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Unitization.instDistribMulAction Semiring.toModule NonUnitalStarAlgHom.instFunLike NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass Unitization.inrNonUnitalStarAlgHom DFunLike.coe ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContinuousMapZero.instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMapZero.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMapZero.instModule SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsSemitopologicalSemiring.toSeparatelyContinuousMul Semiring.toNonUnitalSemiring ContinuousMapZero.instStarRing IsTopologicalRing.toIsTopologicalSemiring RCLike.instContinuousStar NonAssocRing.toNonUnitalNonAssocRing Unitization.instNonAssocRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalSeminormedRing.toPseudoMetricSpace cfcₙAux	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul instFactMemSetQuasispectrumOfNat ContinuousMapZero.instIsScalarTower' IsScalarTower.right ContinuousMapZero.instSMulCommClass' Algebra.to_smulCommClass ContinuousMapZero.instStarModule StarMul.toStarModule Continuous.range_subset_closure_image_dense continuous_cfcₙAux ContinuousMapZero.adjoin_id_dense quasispectrum.instCompactSpace FiniteDimensional.proper_real FiniteDimensional.rclike_to_real NonUnitalStarAlgHom.instNonUnitalAlgHomClass NonUnitalStarAlgHom.instStarHomClass SetLike.mem_coe closure_minimal NonUnitalStarSubalgebra.coe_map SetLike.coe_subset_coe instIsConcreteLE NonUnitalStarSubalgebra.map_le NonUnitalStarAlgebra.adjoin_le Set.singleton_subset_iff NonUnitalStarSubalgebra.mem_comap cfcₙAux_id NonUnitalStarAlgHom.coe_range Set.ext Unitization.ext IsClosed.preimage Unitization.continuous_fst isClosed_singleton T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
cfcₙHom_nnreal_eq_restrict 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	cfcₙHom NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Semifield.toCommSemiring NNReal.instSemifield IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus QuasispectrumRestricts.nonUnitalStarAlgHom NNReal.instTopologicalSpace Real.instField instStarRingReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Real.metricSpace instIsTopologicalRingReal instContinuousStarReal NNReal.instAlgebraOfReal CommSemiring.toSemiring Real.instCommSemiring Algebra.id Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Field.toSemifield IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul Real.pseudoMetricSpace Real.instAdd SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalSemiring StarRing.toStarAddMonoid EuclideanDomain.toNontrivial Field.toEuclideanDomain CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing IsSelfAdjoint.of_nonneg ContinuousMap.realToNNReal QuasispectrumRestricts.nnreal_of_nonneg	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal QuasispectrumRestricts.cfcₙHom_eq_restrict NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NNReal.instContinuousMapZero.UniqueHom QuasispectrumRestricts.nnreal_of_nonneg IsSelfAdjoint.of_nonneg
cfcₙHom_real_eq_restrict 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	cfcₙHom Real IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid Semifield.toCommSemiring Field.toSemifield Real.instField IsDomain.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring instIsDomain instStarRingReal Real.metricSpace IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup IsScalarTower.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus QuasispectrumRestricts.nonUnitalStarAlgHom Complex Complex.instField Complex.instStarRing MetricSpace.toPseudoMetricSpace NormedField.toMetricSpace Complex.instNormedField IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex RCLike.toNormedAlgebra Complex.instRCLike Complex.addCommGroup Complex.instModuleSelf DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left Complex.instSemiring DistribMulAction.toMulAction Complex.instStarModuleReal IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace Real.instZero Complex.instZero Algebra.toSMul NormedSpace.toIsBoundedSMul NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra CommCStarAlgebra.toNonUnitalCommCStarAlgebra IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib EuclideanDomain.toNontrivial Field.toEuclideanDomain CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing IsSelfAdjoint.isStarNormal toContinuousMap ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.instAddCommMonoid NormedSpace.toModule NormedField.toNormedSpace ContinuousLinearMap.funLike ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Complex.reCLM IsSelfAdjoint.quasispectrumRestricts	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar QuasispectrumRestricts.cfcₙHom_eq_restrict instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus RCLike.uniqueNonUnitalContinuousFunctionalCalculus ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass IsSelfAdjoint.isStarNormal IsSelfAdjoint.quasispectrumRestricts
cfcₙ_complex_eq_real 📖	mathematical	Star.star Complex InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex StarRing.toStarAddMonoid Complex.instStarRing IsSelfAdjoint NonUnitalRing.toNonUnitalNonAssocRing	cfcₙ Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid 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 Real IsSelfAdjoint Real.instCommSemiring Real.instNontrivial instStarRingReal Real.metricSpace NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instIsTopologicalRingReal instContinuousStarReal Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup IsScalarTower.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus Complex.re Complex.ofReal	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Real.instNontrivial instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus cfcₙ_real_eq_complex cfcₙ_congr QuasispectrumRestricts.real_iff IsSelfAdjoint.quasispectrumRestricts
cfcₙ_nnreal_eq_real 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	cfcₙ NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NNReal.instCommSemiring NNReal.instNontrivial instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NonUnitalNonAssocSemiring.toAddCommMonoid NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar 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 NNReal.toReal Real.toNNReal	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal QuasispectrumRestricts.cfcₙ_eq_restrict NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal IsScalarTower.left instStarModuleNNRealReal NNReal.instContinuousSMulOfReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus NNReal.instContinuousMapZero.UniqueHom NNReal.isClosedEmbedding_coe IsSelfAdjoint.of_nonneg QuasispectrumRestricts.nnreal_of_nonneg
cfcₙ_real_eq_complex 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid	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 Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup IsScalarTower.complexToReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Complex.instCommSemiring Complex.instNontrivial Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar Complex.ofReal Complex.re	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar QuasispectrumRestricts.cfcₙ_eq_restrict instIsTopologicalRingReal instContinuousStarReal IsScalarTower.complexToReal IsScalarTower.left Complex.instStarModuleReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul SMulCommClass.complexToReal IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus RCLike.uniqueNonUnitalContinuousFunctionalCalculus ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Isometry.isClosedEmbedding Real.instCompleteSpace Complex.isometry_ofReal IsSelfAdjoint.isStarNormal IsSelfAdjoint.quasispectrumRestricts
cfcₙ_real_eq_nnreal 📖	mathematical	Real Real.instLE Real.instZero Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	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 NNReal Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NNReal.instCommSemiring NNReal.instNontrivial instStarRingNNReal instMetricSpaceNNReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instModuleOfReal NNReal.instIsScalarTowerOfReal DistribMulAction.toMulAction Real.instMonoid Module.toDistribMulAction Real.semiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus Real.toNNReal NNReal.toReal	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal NNReal.instIsTopologicalSemiring NNReal.instContinuousStar NNReal.instIsScalarTowerOfReal NNReal.smulCommClass_left Nonneg.instNonUnitalContinuousFunctionalCalculus cfcₙ_nnreal_eq_real cfcₙ_congr Real.coe_toNNReal NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg
commute_iff_mul_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal Commute.mul_nonneg IsSelfAdjoint.commute_iff LE.le.isSelfAdjoint
continuous_cfcₙAux 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	Continuous ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Unitization ContinuousMapZero.instTopologicalSpace Unitization.instUniformSpace DenselyNormedField.toNontriviallyNormedField DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousMapZero.instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMapZero.instModule NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing IsTopologicalRing.toIsTopologicalSemiring RCLike.toStarRing RCLike.instContinuousStar NonAssocRing.toNonUnitalNonAssocRing Unitization.instNonAssocRing NonUnitalRing.toNonUnitalNonAssocRing Unitization.instDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalSeminormedRing.toPseudoMetricSpace Unitization.instStar NonUnitalStarAlgHom.instFunLike cfcₙAux	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsScalarTower.left Continuous.comp IsLocalRing.toNontrivial Field.instIsLocalRing cfcHom_continuous Homeomorph.instContinuousMapClass ContinuousMap.continuous_precomp Topology.IsEmbedding.continuous ContinuousMapZero.instContinuousMapClass ContinuousMapZero.isEmbedding_toContinuousMap
inrNonUnitalStarAlgHom_comp_cfcₙHom_eq_cfcₙAux 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	NonUnitalStarAlgHom.comp ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing 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 NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring ContinuousMapZero.instModule Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing RCLike.toStarRing RCLike.instContinuousStar NonUnitalRing.toNonUnitalSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Unitization.instNonAssocSemiring Unitization.instDistribMulAction Unitization.instStar AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Unitization.inrNonUnitalStarAlgHom cfcₙHom NonUnitalSeminormedRing.toPseudoMetricSpace RCLike.nonUnitalContinuousFunctionalCalculus cfcₙAux	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsScalarTower.left ContinuousMapZero.UniqueHom.eq_of_continuous_of_map_id CStarRing.instRegularNormedAlgebra IsScalarTower.right Algebra.to_smulCommClass RCLike.uniqueNonUnitalContinuousFunctionalCalculus Unitization.instT2Space NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum IsLocalRing.toNontrivial Field.instIsLocalRing RCLike.nonUnitalContinuousFunctionalCalculus instFactMemSetQuasispectrumOfNat IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Continuous.comp Unitization.continuous_inr cfcₙHom_continuous continuous_cfcₙAux cfcₙHom_id cfcₙAux_id
isClosedEmbedding_cfcₙAux 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	Topology.IsClosedEmbedding ContinuousMapZero Set.Elem quasispectrum Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing quasispectrum.instZero IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Unitization ContinuousMapZero.instTopologicalSpace Unitization.instUniformSpace DenselyNormedField.toNontriviallyNormedField DFunLike.coe NonUnitalStarAlgHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero ContinuousMapZero.instNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Module.toDistribMulAction ContinuousMapZero.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMapZero.instModule NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing IsTopologicalRing.toIsTopologicalSemiring RCLike.toStarRing RCLike.instContinuousStar NonAssocRing.toNonUnitalNonAssocRing Unitization.instNonAssocRing NonUnitalRing.toNonUnitalNonAssocRing Unitization.instDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup NonUnitalSeminormedRing.toPseudoMetricSpace Unitization.instStar NonUnitalStarAlgHom.instFunLike cfcₙAux	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Topology.IsClosedEmbedding.comp ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus cfcHom_isClosedEmbedding Unitization.quasispectrum_eq_spectrum_inr' Homeomorph.isClosedEmbedding ContinuousMapZero.isClosedEmbedding_toContinuousMap T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing StarRing.toStarAddMonoid IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib QuasispectrumRestricts Real Complex Real.instCommSemiring Complex.instCommSemiring Module.complexToReal NonUnitalNonAssocRing.toAddCommGroup NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex RCLike.toNormedAlgebra Complex.instRCLike DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Complex.instNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedSpace.complexToReal NormedField.toNormedSpace Real.normedCommRing ContinuousLinearMap.funLike Complex.reCLM	—	Complex.instNontrivial IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsSelfAdjoint.isStarNormal eqOn_of_cfcₙ_eq_cfcₙ IsSelfAdjoint.star_eq cfcₙ_id cfcₙ_star ContinuousOn.star continuousOn_id' star_zero Complex.conj_eq_iff_re Complex.ofReal_re isSelfAdjoint_iff cfcₙ_star_id cfcₙ_congr QuasispectrumRestricts.algebraMap_image IsScalarTower.complexToReal IsScalarTower.left Complex.conj_ofReal
nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid QuasispectrumRestricts NNReal Real NNReal.instCommSemiring Real.instCommSemiring NNReal.instModuleOfReal NNReal.instAlgebraOfReal CommSemiring.toSemiring Algebra.id DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace ContinuousMap.instFunLike ContinuousMap.realToNNReal	—	Real.instNontrivial IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousStarReal IsSelfAdjoint.of_nonneg QuasispectrumRestricts.nnreal_of_nonneg CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts IsSelfAdjoint.star_eq star_mul_self_nonneg
spec_cfcₙAux 📖	mathematical	Unitization.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	spectrum Unitization Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField Unitization.instRing EuclideanDomain.toCommRing Field.toEuclideanDomain NonUnitalNormedRing.toNonUnitalRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Unitization.instAlgebra CommRing.toCommSemiring NonUnitalRing.toNonUnitalSemiring Algebra.id Module.toDistribMulAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace NonUnitalSeminormedRing.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid DFunLike.coe NonUnitalStarAlgHom ContinuousMapZero Set.Elem quasispectrum quasispectrum.instZero IsLocalRing.toNontrivial Field.instIsLocalRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing instTopologicalSpaceSubtype Set Set.instMembership SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ContinuousMapZero.instNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousMapZero.instAddCommMonoid NonUnitalNormedCommRing.toNonUnitalNormedRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing ContinuousMapZero.instModule NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid ContinuousMapZero.instStarRing IsTopologicalRing.toIsTopologicalSemiring RCLike.toStarRing RCLike.instContinuousStar NonAssocRing.toNonUnitalNonAssocRing Unitization.instNonAssocRing NonUnitalRing.toNonUnitalNonAssocRing Unitization.instDistribMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing NonUnitalNonAssocRing.toAddCommGroup Unitization.instStar NonUnitalStarAlgHom.instFunLike cfcₙAux Set.range ContinuousMapZero.instFunLike	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsScalarTower.left IsLocalRing.toNontrivial Field.instIsLocalRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul cfcₙAux.eq_1 NonUnitalStarAlgHom.comp_assoc NonUnitalStarAlgHom.comp_apply ClosedEmbeddingContinuousFunctionalCalculus.toContinuousFunctionalCalculus cfcHom_map_spectrum EquivLike.range_comp

---

← Back to Index