mem_spectrum_iff_exists — Mathlib

English

For any a ∈ A and z ∈ ℂ, z lies in the spectrum of a if and only if there exists a character f with f(a) = z.

Русский

Для любого a и z ∈ ℂ, z принадлежит спектру a тогда и только тогда существует характер f с f(a) = z.

LaTeX

$$$$z \in \sigma_\mathbb{C}(a) \iff \exists f \text{ in } \text{characterSpace}(\mathbb{C},A), f(a) = z$$$$

Lean4

theorem mem_spectrum_iff_exists {a : A} {z : ℂ} : z ∈ spectrum ℂ a ↔ ∃ f : characterSpace ℂ A, f a = z :=
  by
  refine ⟨fun hz => ?_, ?_⟩
  · obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz
    simp only [map_sub, sub_eq_zero, AlgHomClass.commutes] at hf
    exact ⟨_, hf.symm⟩
  · rintro ⟨f, rfl⟩
    exact AlgHom.apply_mem_spectrum f a

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