Instances

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

Statistics

Metric	Count
Definitions `cfcₙAux`	1
Theorems `exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts`, `exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts`, `mul_nonneg`, `instContinuousFunctionalCalculus`, `instNonUnitalContinuousFunctionalCalculus`, `quasispectrumRestricts`, `spectrumRestricts`, `spectrum_nonempty`, `commute_iff`, `spectrum_nonempty`, `instContinuousFunctionalCalculus`, `instNonUnitalContinuousFunctionalCalculus`, `isSelfAdjoint`, `nonUnitalContinuousFunctionalCalculus`, `isSelfAdjoint`, `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_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`, `isClosedEmbedding_cfcₙAux`, `isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts`, `isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts`, `nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts`, `nonneg_iff_isSelfAdjoint_and_spectrumRestricts`, `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` `instCommSemiringNNReal` `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`
`exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `QuasispectrumRestricts` `NNReal` `Real` `instCommSemiringNNReal` `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`	—	`exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts`

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_nonneg` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Commute` `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` `Real.instCompleteSpace` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Isometry.isUniformEmbedding` `Complex.isometry_ofReal` `zero` `isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts` `IsScalarTower.right` `Algebra.to_smulCommClass` `ContinuousFunctionalCalculus.toNonUnital` `Complex.instCompleteSpace`
`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` `Real.instCompleteSpace` `SMulCommClass.complexToReal` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Isometry.isUniformEmbedding` `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` `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` `Complex.instCompleteSpace`
`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` `CFC.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`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `commute_iff_mul_nonneg` `IsScalarTower.right` `Algebra.to_smulCommClass` `ContinuousFunctionalCalculus.toNonUnital` `Real.instCompleteSpace` `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` `instCommSemiringNNReal`	—	`instIsTopologicalSemiring` `instContinuousStar` `CFC.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` `instCommSemiringNNReal` `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.instCompleteSpace` `isUniformEmbedding_subtype_val` `le_rfl` `nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts` `IsScalarTower.right` `Algebra.to_smulCommClass` `ContinuousFunctionalCalculus.toNonUnital` `Real.instCompleteSpace`
`instNonUnitalContinuousFunctionalCalculus` 📖	mathematical	—	`NonUnitalContinuousFunctionalCalculus` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `instCommSemiringNNReal` `instNontrivialNNReal` `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.instCompleteSpace` `NNReal.smulCommClass_left` `isUniformEmbedding_subtype_val` `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` `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` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.instIsLocalRing` `toStarRing` `NormedField.toMetricSpace` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `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` `quasispectrum.instCompactSpace` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `IsTopologicalSemiring.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `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` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `Topology.IsClosedEmbedding.of_comp_iff` `Isometry.isClosedEmbedding` `Unitization.isometry_inr` `isClosedEmbedding_cfcₙAux` `Unitization.inr_injective` `cfcₙAux_id` `spec_cfcₙAux` `Unitization.quasispectrum_eq_spectrum_inr'` `cfcHom_predicate`

SpectrumRestricts

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` `StarRing.toStarAddMonoid`	—	`QuasispectrumRestricts.isSelfAdjoint`

(root)

Definitions

Name	Category	Theorems
`cfcₙAux` 📖	CompOp	5 math math: `isClosedEmbedding_cfcₙAux`, `cfcₙAux_id`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `spec_cfcₙAux`, `cfcₙAux_mem_range_inr`

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` `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` `NNReal.instCompleteSpace` `Nonneg.instContinuousFunctionalCalculus` `NNReal.instContinuousMap.UniqueHom` `isUniformEmbedding_subtype_val` `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` `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` `Real.instCompleteSpace` `IsSelfAdjoint.instContinuousFunctionalCalculus` `Real.instContinuousMapUniqueHom` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Isometry.isUniformEmbedding` `Complex.isometry_ofReal` `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` `IsStarNormal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Complex.instCommSemiring` `NormedField.toMetricSpace` `Complex.instNormedField` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instContinuousStar` `Real` `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` `instCommSemiringNNReal` `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` `NNReal.instCompleteSpace` `Nonneg.instContinuousFunctionalCalculus` `NNReal.instContinuousMap.UniqueHom` `isUniformEmbedding_subtype_val` `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` `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` `Real.instCompleteSpace` `IsSelfAdjoint.instContinuousFunctionalCalculus` `Real.instContinuousMapUniqueHom` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Isometry.isUniformEmbedding` `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` `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` `instCommSemiringNNReal` `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` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `quasispectrum.instZero` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.instIsLocalRing` `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` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousMapZero.instModule` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `RCLike.toStarRing` `RCLike.instContinuousStar` `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`	—	`IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `IsScalarTower.left` `cfcHom_id`
`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` `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.toNormedSpace` `Unitization.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `StarRing.toStarAddMonoid` `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` `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` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousMapZero.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousMapZero.instStarRing` `RCLike.instContinuousStar` `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` `IsTopologicalSemiring.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `instFactMemSetQuasispectrumOfNat` `ContinuousMapZero.instIsScalarTower'` `IsScalarTower.right` `ContinuousMapZero.instSMulCommClass'` `Algebra.to_smulCommClass` `ContinuousMapZero.instStarModule` `StarMul.toStarModule` `Continuous.range_subset_closure_image_dense` `Topology.IsClosedEmbedding.continuous` `isClosedEmbedding_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` `Continuous.fst` `UniformEquiv.continuous` `NonUnitalStarAlgHom.coe_range` `Set.ext` `Unitization.ext` `IsClosed.preimage` `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` `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.instCompleteSpace` `NNReal.smulCommClass_left` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `NNReal.instContinuousMapZero.UniqueHom` `isUniformEmbedding_subtype_val` `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` `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` `Real.instCompleteSpace` `SMulCommClass.complexToReal` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `RCLike.uniqueNonUnitalContinuousFunctionalCalculus` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Isometry.isUniformEmbedding` `Complex.isometry_ofReal` `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ₙ` `IsStarNormal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Complex.instCommSemiring` `Complex.instNontrivial` `NormedField.toMetricSpace` `Complex.instNormedField` `IsTopologicalRing.toIsTopologicalSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instContinuousStar` `Real` `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` `instCommSemiringNNReal` `instNontrivialNNReal` `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.instCompleteSpace` `NNReal.smulCommClass_left` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `NNReal.instContinuousMapZero.UniqueHom` `isUniformEmbedding_subtype_val` `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` `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` `Real.instCompleteSpace` `SMulCommClass.complexToReal` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `RCLike.uniqueNonUnitalContinuousFunctionalCalculus` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Isometry.isUniformEmbedding` `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ₙ` `IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `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` `instCommSemiringNNReal` `instNontrivialNNReal` `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`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `Commute.mul_nonneg` `IsSelfAdjoint.commute_iff` `LE.le.isSelfAdjoint`
`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` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `quasispectrum.instZero` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.instIsLocalRing` `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` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousMapZero.instModule` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `RCLike.toStarRing` `RCLike.instContinuousStar` `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` `IsTopologicalSemiring.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Topology.IsClosedEmbedding.comp` `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`
`isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts` 📖	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`	—	`isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts`
`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` `instCommSemiringNNReal` `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`
`nonneg_iff_isSelfAdjoint_and_spectrumRestricts` 📖	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` `instCommSemiringNNReal` `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`	—	`nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts`
`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` `Unitization.instRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `Unitization.instAlgebra` `NonUnitalRing.toNonUnitalSemiring` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `Set.Elem` `quasispectrum` `quasispectrum.instZero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `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` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `ContinuousMapZero.instModule` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `ContinuousMapZero.instStarRing` `RCLike.toStarRing` `RCLike.instContinuousStar` `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` `IsTopologicalSemiring.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `cfcₙAux.eq_1` `NonUnitalStarAlgHom.comp_assoc` `NonUnitalStarAlgHom.comp_apply` `cfcHom_map_spectrum` `EquivLike.range_comp`

---

← Back to Index