Documentation Verification Report

Commute

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

Statistics

Metric	Count
Definitions	0
Theorems `cfc`, `cfcHom`, `cfc_nnreal`, `cfc_real`, `cfcₙ`, `cfcₙHom`, `cfcₙ_nnreal`, `cfcₙ_real`, `commute_cfc`, `commute_cfcHom`, `commute_cfcₙ`, `commute_cfcₙHom`	12
Total	12

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cfc` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`cfc` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.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` `RCLike.instContinuousStar`	—	`IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `cfc_cases` `zero_left` `cfcHom` `ContinuousOn.restrict`
`cfcHom` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`DFunLike.coe` `StarAlgHom` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedField.toMetricSpace` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RCLike.toStarRing` `RCLike.instContinuousStar` `Ring.toSemiring` `StarAlgHom.instFunLike` `cfcHom`	—	`IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `ContinuousMap.induction_on_of_compact` `ContinuousFunctionalCalculus.compactSpace_spectrum` `AlgHomClass.commutes` `StarAlgHom.instAlgHomClass` `Algebra.commute_algebraMap_left` `cfcHom_id` `StarHomClass.map_star` `StarAlgHom.instStarHomClass` `IsTopologicalSemiring.toContinuousAdd` `map_add` `SemilinearMapClass.toAddHomClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `add_left` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `mul_left` `commute_iff_eq` `Set.mem_setOf` `IsClosed.closure_eq` `isClosed_eq` `Continuous.fun_mul` `continuous_id'` `continuous_const` `mem_closure_of_frequently_of_tendsto` `Continuous.tendsto` `cfcHom_continuous`
`cfc_nnreal` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`cfc` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instCommSemiringNNReal` `instStarRingNNReal` `instMetricSpaceNNReal` `NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `NNReal.instAlgebraOfReal` `Ring.toSemiring` `Nonneg.instContinuousFunctionalCalculus`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `Nonneg.instContinuousFunctionalCalculus` `cfc_nnreal_eq_real` `cfc_real` `cfc_apply_of_not_predicate`
`cfc_real` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`cfc` `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`	—	`IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `cfc_cases` `zero_left` `ContinuousOn.restrict` `cfc_apply` `cfc` `IsSelfAdjoint.star_eq`
`cfcₙ` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`cfcₙ` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.instIsLocalRing` `RCLike.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` `RCLike.instContinuousStar`	—	`IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `cfcₙ_cases` `zero_left` `ContinuousOn.restrict` `cfcₙHom`
`cfcₙHom` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `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` `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` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMapZero.instModule` `Semiring.toModule` `SMulCommClass.continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.to_smulCommClass` `Algebra.id` `IsTopologicalSemiring.toContinuousMul` `Semiring.toNonUnitalSemiring` `ContinuousMapZero.instStarRing` `RCLike.toStarRing` `RCLike.instContinuousStar` `NonUnitalStarAlgHom.instFunLike` `cfcₙHom`	—	`IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `ContinuousMapZero.induction_on_of_compact` `instFactMemSetQuasispectrumOfNat` `NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum` `IsTopologicalSemiring.toContinuousAdd` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `NonUnitalStarAlgHom.instNonUnitalAlgHomClass` `cfcₙHom_id` `StarHomClass.map_star` `NonUnitalStarAlgHom.instStarHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalAlgHomClass.instLinearMapClass` `add_left` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `mul_left` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `smul_left` `commute_iff_eq` `Set.mem_setOf` `IsClosed.closure_eq` `isClosed_eq` `Continuous.fun_mul` `continuous_id'` `continuous_const` `mem_closure_of_frequently_of_tendsto` `Continuous.tendsto` `cfcₙHom_continuous`
`cfcₙ_nnreal` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	`cfcₙ` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `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`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `NNReal.instIsTopologicalSemiring` `NNReal.instContinuousStar` `NNReal.instIsScalarTowerOfReal` `NNReal.smulCommClass_left` `Nonneg.instNonUnitalContinuousFunctionalCalculus` `cfcₙ_nnreal_eq_real` `cfcₙ_real` `cfcₙ_apply_of_not_predicate`
`cfcₙ_real` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing`	`cfcₙ` `Real` `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`	—	`Real.instNontrivial` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instContinuousStarReal` `cfcₙ_cases` `zero_left` `ContinuousOn.restrict` `IsTopologicalSemiring.toContinuousAdd` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `cfcₙ_apply` `cfcₙ` `IsSelfAdjoint.star_eq`

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute_cfc` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`cfc` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.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` `RCLike.instContinuousStar`	—	`IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `Commute.cfc` `star_eq`
`commute_cfcHom` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`DFunLike.coe` `StarAlgHom` `ContinuousMap` `Set.Elem` `spectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedField.toMetricSpace` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RCLike.toStarRing` `RCLike.instContinuousStar` `Ring.toSemiring` `StarAlgHom.instFunLike` `cfcHom`	—	`IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `Commute.cfcHom` `star_eq`
`commute_cfcₙ` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`cfcₙ` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.instIsLocalRing` `RCLike.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` `RCLike.instContinuousStar`	—	`IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `Commute.cfcₙ` `star_eq`
`commute_cfcₙHom` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `StarRing.toStarAddMonoid` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`DFunLike.coe` `NonUnitalStarAlgHom` `ContinuousMapZero` `Set.Elem` `quasispectrum` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `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` `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` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMapZero.instModule` `Semiring.toModule` `SMulCommClass.continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Algebra.to_smulCommClass` `Algebra.id` `IsTopologicalSemiring.toContinuousMul` `Semiring.toNonUnitalSemiring` `ContinuousMapZero.instStarRing` `RCLike.toStarRing` `RCLike.instContinuousStar` `NonUnitalStarAlgHom.instFunLike` `cfcₙHom`	—	`IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `Commute.cfcₙHom` `star_eq`

---

← Back to Index