English
Let a ∈ A and p ∈ 𝕜[X], with (σ a).Nonempty. Then σ(aeval a p) = { eval_x(p) : x ∈ σ(a) }. This is the nonempty-spectrum version of the polynomial spectral mapping theorem.
Русский
Пусть a ∈ A и p ∈ 𝕜[X], и спектр a непуст. Тогда σ(aeval_a(p)) = { eval_x(p) : x ∈ σ(a) }. Это версия теоремы о спектральном отображении для полиномов при непустом спектре.
LaTeX
$$$$ (\\sigma a).Nonempty \\Rightarrow \\sigma\\big(\\mathrm{aeval}_a p\\big) = \\{ \\operatorname{eval}(x,p) : x \\in \\sigma(a) \\}. $$$$
Lean4
/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
convenience. -/
theorem map_pow_of_nonempty [IsAlgClosed 𝕜] {a : A} (ha : (σ a).Nonempty) (n : ℕ) : σ (a ^ n) = (· ^ n) '' σ a := by
simpa only [aeval_X_pow, eval_X_pow] using map_polynomial_aeval_of_nonempty a (X ^ n) ha
