gelfandTransform_eq — Mathlib

English

The Gelfand transform preserves spectra: for any a ∈ A, σ_ℂ(gelfandTransform(a)) = σ_ℂ(a).

Русский

Гельфанд-преобразование сохраняет спектры: для любого a, σ_ℂ(gelfandTransform(a)) = σ_ℂ(a).

LaTeX

$$$$\sigma_{\mathbb{C}}(\,\mathrm{gelfandTransform}(\mathbb{C},A,a)\,) = \sigma_{\mathbb{C}}(a)$$$$

Lean4

/-- The Gelfand transform is spectrum-preserving. -/
theorem gelfandTransform_eq (a : A) : spectrum ℂ (gelfandTransform ℂ A a) = spectrum ℂ a :=
  by
  ext z
  rw [ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists]
  exact Iff.rfl

Похожие утверждения