English
For any a ∈ A and any n ≥ 1, the spectrum of a^n is the image of the spectrum of a under the map x ↦ x^n: σ(a^n) = { x^n : x ∈ σ(a) }. This specializes the general spectral mapping to monomial polynomials.
Русский
Для любого a ∈ A и любого n ≥ 1 спектр a^n есть образ спектра a при отображении x ↦ x^n: σ(a^n) = { x^n : x ∈ σ(a) }. Это частный случай общего спектрального отображения для монономомов.
LaTeX
$$$$ \\sigma(a^n) = \\{ x^n \\;|\; x \\in \\sigma(a) \\}. $$$$
Lean4
/-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/
theorem pow_image_subset (a : A) (n : ℕ) : (fun x => x ^ n) '' σ a ⊆ σ (a ^ n) := by
simpa only [eval_X_pow, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])
