Theorems · Theorem · functional analysis

spectrum.gelfandTransform_eq

∀ {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] (a : A),
  spectrum ℂ ((WeakDual.gelfandTransform ℂ A) a) = spectrum ℂ a

The Gelfand transform is spectrum-preserving.

Defined in: Mathlib.Analysis.CStarAlgebra.GelfandDuality
Cited by: 1 results in Mathlib
Foundations: Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedCommRing NormedAlgebra CompleteSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Set.Elemstatement · cited by 7,166
Complexstatement and proof · cited by 5,565
Set.rangeproof · cited by 4,705
AlgHomstatement · cited by 3,236
CompleteSpacestatement and proof · cited by 2,532
ContinuousMapstatement · cited by 2,491
Set.extproof · cited by 2,266
NormedAlgebrastatement and proof · cited by 1,165
spectrumstatement and proof · cited by 510
NormedCommRingstatement and proof · cited by 218

Cited by1

Results whose statement or proof uses this declaration.

gelfandTransform_isometryproof · cited by 2