map_polynomial_aeval — Mathlib

English

Specialization of the spectral mapping theorem to monic monomials: spectrum of a^n equals the image {λ^n : λ ∈ spectrum(a)}.

Русский

Специализация спектрального отображения для мономов: спектр $a^n$ равен образу спектра $a$ под отображением $\\lambda \\mapsto \\lambda^n$.

LaTeX

$$$\\mathrm{spec}_{\\mathbb{C}}(a^n) = \\{ \\lambda^n : \\lambda \\in \\mathrm{spec}_{\\mathbb{C}}(a) \\}$$$

Lean4

/-- The **spectral mapping theorem** for polynomials in a Banach algebra over `ℂ`. -/
theorem map_polynomial_aeval (a : A) (p : ℂ[X]) : spectrum ℂ (aeval a p) = (fun k => eval k p) '' spectrum ℂ a :=
  map_polynomial_aeval_of_nonempty a p (spectrum.nonempty a)

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