Documentation Verification Report

GelfandDuality

📁 Source: Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

Statistics

Metric	Count
Definitions `toCharacterSpace`, `compContinuousMap`, `gelfandStarTransform`	3
Theorems `toCharacterSpace_apply_eq_zero_of_mem`, `compContinuousMap_apply`, `compContinuousMap_comp`, `compContinuousMap_id`, `exists_apply_eq_zero`, `homeoEval_naturality`, `mem_spectrum_iff_exists`, `gelfandStarTransform_apply_apply`, `gelfandStarTransform_naturality`, `gelfandStarTransform_symm_apply`, `gelfandTransform_bijective`, `gelfandTransform_isometry`, `gelfandTransform_map_star`, `instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial`, `gelfandTransform_eq`	15
Total	18

Ideal

Definitions

Name	Category	Theorems
`toCharacterSpace` 📖	CompOp	1 math math: `toCharacterSpace_apply_eq_zero_of_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCharacterSpace_apply_eq_zero_of_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `Set.Elem` `WeakDual` `Complex` `Complex.instCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NormedAlgebra.toNormedSpace` `WeakDual.characterSpace` `WeakDual.CharacterSpace.instFunLike` `toCharacterSpace` `Complex.instZero`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `spectrum.nonempty` `instIsTwoSided_1` `Quotient.eq_zero_iff_mem` `Set.Nonempty.some.congr_simp` `spectrum.zero_eq` `IsDomain.toNontrivial` `Quotient.isDomain` `IsMaximal.isPrime'` `Set.eq_of_mem_singleton` `Set.Nonempty.some_mem` `Set.singleton_nonempty`

WeakDual.CharacterSpace

Definitions

Name	Category	Theorems
`compContinuousMap` 📖	CompOp	5 math math: `gelfandStarTransform_naturality`, `homeoEval_naturality`, `compContinuousMap_apply`, `compContinuousMap_comp`, `compContinuousMap_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compContinuousMap_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `WeakDual` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedSpace.toModule` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NormedRing.toSeminormedRing` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `ContinuousMap.instFunLike` `compContinuousMap` `Equiv` `AlgHom` `Ring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NormedAlgebra.toAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivAlgHom` `AlgHom.comp` `StarAlgHom.toAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul`
`compContinuousMap_comp` 📖	mathematical	—	`compContinuousMap` `StarAlgHom.comp` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `ContinuousMap.comp` `Set.Elem` `WeakDual` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NormedSpace.toModule` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual`	—	`ContinuousMap.ext` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `ext`
`compContinuousMap_id` 📖	mathematical	—	`compContinuousMap` `StarAlgHom.id` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Ring.toSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedRing.toSeminormedRing` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `ContinuousMap.id` `Set.Elem` `WeakDual` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NormedSpace.toModule` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual`	—	`ContinuousMap.ext` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `ext`
`exists_apply_eq_zero` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing`	`DFunLike.coe` `Set.Elem` `WeakDual` `Complex` `Complex.instCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NormedAlgebra.toNormedSpace` `WeakDual.characterSpace` `instFunLike` `Complex.instZero`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Ideal.exists_le_maximal` `Ideal.span_singleton_ne_top` `Ideal.toCharacterSpace_apply_eq_zero_of_mem` `Ideal.mem_span_singleton` `mul_one`
`homeoEval_naturality` 📖	mathematical	—	`ContinuousMap.comp` `Set.Elem` `WeakDual` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `ContinuousMap.instNormedRing` `NormedSpace.toModule` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NormedRing.toSeminormedRing` `ContinuousMap.instNormedAlgebra` `NormedAlgebra.id` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `toContinuousMap` `Homeomorph` `ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring` `ContinuousMap.module` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedField.toNormedSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `ContinuousMap.compactOpen` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.instContinuousMapClass` `homeoEval` `compContinuousMap` `ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace` `RCLike.toCompleteSpace` `CompactlyCoherentSpace.of_weaklyLocallyCompactSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `ContinuousMap.instStarRingOfContinuousStar` `RCLike.toStarRing` `RCLike.instContinuousStar` `ContinuousMap.compStarAlgHom'` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Homeomorph.instContinuousMapClass`
`mem_spectrum_iff_exists` 📖	mathematical	—	`Complex` `Set` `Set.instMembership` `spectrum` `Complex.instCommSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `DFunLike.coe` `Set.Elem` `WeakDual` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NormedAlgebra.toNormedSpace` `WeakDual.characterSpace` `instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `exists_apply_eq_zero` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `instNonUnitalAlgHomClass` `AlgHomClass.commutes` `instAlgHomClass` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `AlgHom.apply_mem_spectrum` `Complex.instNontrivial`

(root)

Definitions

Name	Category	Theorems
`gelfandStarTransform` 📖	CompOp	3 math math: `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `gelfandStarTransform_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gelfandStarTransform_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `WeakDual` `Complex` `Complex.instCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NonUnitalCStarAlgebra.toNormedSpace` `NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `ContinuousMap.instFunLike` `StarAlgEquiv` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `ContinuousMap.instAdd` `Complex.instAdd` `Distrib.toMul` `ContinuousMap.instMul` `Complex.instMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `ContinuousMap.instSMul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `ContinuousMap.instStar` `Complex.instStarRing` `Complex.instContinuousStar` `StarAlgEquiv.instFunLike` `gelfandStarTransform` `CommRing.toCommSemiring` `Complex.commRing` `NormedCommRing.toCommRing` `Algebra.toModule` `WeakDual.CharacterSpace.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Complex.instContinuousStar`
`gelfandStarTransform_naturality` 📖	mathematical	—	`StarAlgHom.comp` `Complex` `ContinuousMap` `Set.Elem` `WeakDual` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `CStarAlgebra.toNormedRing` `CommCStarAlgebra.toCStarAlgebra` `NormedSpace.toModule` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedAlgebra.toNormedSpace` `NormedRing.toSeminormedRing` `CStarAlgebra.toNormedAlgebra` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `Complex.instCommSemiring` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `NormedAlgebra.toAlgebra` `Complex.instNormedField` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `Complex.instSemiring` `ContinuousMap.algebra` `ContinuousMap.instStar` `Complex.instStarRing` `Complex.instContinuousStar` `StarAlgHomClass.toStarAlgHom` `StarAlgEquiv` `Complex.instRing` `NonUnitalCStarAlgebra.toNormedSpace` `NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `ContinuousMap.instAdd` `Complex.instAdd` `Distrib.toMul` `ContinuousMap.instMul` `Complex.instMul` `Ring.toSemiring` `SeminormedRing.toRing` `ContinuousMap.instSMul` `StarAlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `StarAlgEquiv.instEquivLike` `instAlgEquivClassOfNonUnitalAlgEquivClass` `StarAlgEquiv.instNonUnitalAlgEquivClass` `NonUnitalStarRingHomClass.toStarHomClass` `ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring` `RingEquivClass.toNonUnitalRingHomClass` `NonUnitalAlgEquivClass.toRingEquivClass` `StarRingEquivClass.instNonUnitalStarRingHomClass` `StarAlgEquiv.instStarRingEquivClass` `gelfandStarTransform` `ContinuousMap.compStarAlgHom'` `WeakDual.CharacterSpace.compContinuousMap` `CStarAlgebra.toCompleteSpace`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Complex.instContinuousStar` `AlgEquivClass.toAlgHomClass` `instAlgEquivClassOfNonUnitalAlgEquivClass` `StarAlgEquiv.instNonUnitalAlgEquivClass` `NonUnitalStarRingHomClass.toStarHomClass` `RingEquivClass.toNonUnitalRingHomClass` `NonUnitalAlgEquivClass.toRingEquivClass` `StarRingEquivClass.instNonUnitalStarRingHomClass` `StarAlgEquiv.instStarRingEquivClass`
`gelfandStarTransform_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Complex` `ContinuousMap` `Set.Elem` `WeakDual` `Complex.instCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedSpace.toModule` `NonUnitalCStarAlgebra.toNormedSpace` `NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `ContinuousMap.instAdd` `Complex.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `ContinuousMap.instMul` `Complex.instMul` `Distrib.toMul` `ContinuousMap.instSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `Complex.instStarRing` `Complex.instContinuousStar` `CStarAlgebra.toStarRing` `StarAlgEquiv.instFunLike` `StarAlgEquiv.symm` `gelfandStarTransform` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `EquivLike.toEquiv` `RingEquiv` `ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring` `RingEquiv.instEquivLike` `RingEquiv.ofBijective` `StarAlgHom` `CommRing.toCommSemiring` `NormedCommRing.toCommRing` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `Complex.instSemiring` `ContinuousMap.algebra` `StarAlgHom.instFunLike` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `ContinuousMap.instDistribMulActionOfContinuousConstSMul` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Complex.instModuleSelf` `WeakDual.gelfandTransform` `Complex.commRing` `gelfandTransform_map_star` `gelfandTransform_bijective`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `Complex.instContinuousStar`
`gelfandTransform_bijective` 📖	mathematical	—	`Function.Bijective` `ContinuousMap` `Set.Elem` `WeakDual` `Complex` `CommRing.toCommSemiring` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.toSMul` `Algebra.id` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedCommRing.toCommRing` `Algebra.toModule` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `DFunLike.coe` `AlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `AlgHom.funLike` `WeakDual.gelfandTransform` `NormMulClass.toNoZeroDivisors` `CStarAlgebra.toNormedRing` `NormedDivisionRing.toNormMulClass`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Isometry.injective` `WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace` `CStarAlgebra.toCompleteSpace` `Complex.instProperSpace` `gelfandTransform_isometry` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `Complex.instContinuousStar` `CStarAlgebra.toStarModule` `ContinuousMap.ext` `StarHomClass.map_star` `WeakDual.CharacterSpace.instStarHomClass` `ContinuousMap.instIsTopologicalSemiringOfLocallyCompactSpace` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1SpaceSubtype` `instR1Space` `IsTopologicalAddGroup.regularSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `WeakDual.instIsTopologicalAddGroup` `instWeaklyLocallyCompactSpaceOfCompactSpace` `NormedStarGroup.to_continuousStar` `ContinuousMap.instNormedStarGroup` `CStarRing.to_normedStarGroup` `CStarAlgebra.toCStarRing` `le_antisymm` `StarSubalgebra.topologicalClosure_minimal` `le_rfl` `Topology.IsClosedEmbedding.isClosed_range` `Isometry.isClosedEmbedding` `StarSubalgebra.le_topologicalClosure` `ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints` `Mathlib.Tactic.Contrapose.contrapose₂` `RCLike.instContinuousStar` `ContinuousMap.instStarModule` `StarMul.toStarModule` `Mathlib.Tactic.Push.not_and_eq` `ContinuousLinearMap.ext` `StarSubalgebra.mem_top`
`gelfandTransform_isometry` 📖	mathematical	—	`Isometry` `ContinuousMap` `Set.Elem` `WeakDual` `Complex` `CommRing.toCommSemiring` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.toSMul` `Algebra.id` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedCommRing.toCommRing` `Algebra.toModule` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedRing.toMetricSpace` `CStarAlgebra.toNormedRing` `ContinuousMap.instMetricSpace` `WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `CStarAlgebra.toCompleteSpace` `Complex.instProperSpace` `NormedField.toMetricSpace` `DFunLike.coe` `AlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `AlgHom.funLike` `WeakDual.gelfandTransform` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`	—	`AddMonoidHomClass.isometry_of_norm` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace` `CStarAlgebra.toCompleteSpace` `Complex.instProperSpace` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `spectrum.gelfandTransform_eq` `NNReal.sqrt_sq` `Complex.instContinuousStar` `CStarRing.nnnorm_star_mul_self` `ContinuousMap.instCStarRing` `CStarAlgebra.toCStarRing` `IsSelfAdjoint.spectralRadius_eq_nnnorm` `IsSelfAdjoint.star_mul_self` `gelfandTransform_map_star` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass`
`gelfandTransform_map_star` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Complex` `ContinuousMap` `Set.Elem` `WeakDual` `CommRing.toCommSemiring` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.toSMul` `Algebra.id` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedCommRing.toCommRing` `Algebra.toModule` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `CommCStarAlgebra.toCStarAlgebra` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `AlgHom.funLike` `WeakDual.gelfandTransform` `NormMulClass.toNoZeroDivisors` `CStarAlgebra.toNormedRing` `NormedDivisionRing.toNormMulClass` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `ContinuousMap.instStar` `Complex.instStarRing` `Complex.instContinuousStar`	—	`ContinuousMap.ext` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Complex.instContinuousStar` `StarHomClass.map_star` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `WeakDual.CharacterSpace.instStarHomClass`
`instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial` 📖	mathematical	—	`Set.Elem` `WeakDual` `Complex` `Complex.instCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Algebra.toSMul` `Algebra.id` `Ring.uniformContinuousConstSMul` `Complex.instRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NormedAlgebra.toNormedSpace` `WeakDual.characterSpace`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `WeakDual.CharacterSpace.exists_apply_eq_zero` `zero_mem_nonunits` `zero_ne_one` `NeZero.one`

spectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gelfandTransform_eq` 📖	mathematical	—	`spectrum` `Complex` `ContinuousMap` `Set.Elem` `WeakDual` `CommRing.toCommSemiring` `Complex.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.toSMul` `Algebra.id` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedCommRing.toCommRing` `Algebra.toModule` `NormedAlgebra.toAlgebra` `WeakDual.characterSpace` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `instTopologicalSpaceWeakDual` `Complex.instCommSemiring` `ContinuousMap.instRing` `Complex.instRing` `ContinuousMap.algebra` `Complex.instSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `DFunLike.coe` `AlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `AlgHom.funLike` `WeakDual.gelfandTransform` `NormMulClass.toNoZeroDivisors` `CStarAlgebra.toNormedRing` `CommCStarAlgebra.toCStarAlgebra` `NormedDivisionRing.toNormMulClass` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Set.ext` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `ContinuousMap.spectrum_eq_range` `Complex.instCompleteSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `WeakDual.CharacterSpace.mem_spectrum_iff_exists`

---

← Back to Index