map_pow_of_pos — Mathlib

English

A specialization of the nonempty-spectrum result to p = X^n, 0 < n. Then σ(a^n) = { x^n : x ∈ σ(a) } as a corollary of the polynomial spectral mapping theorem for monomials.

Русский

Уточнение для p = X^n, 0 < n: σ(a^n) = { x^n : x ∈ σ(a) } по теореме спектрального отображения для монономов.

LaTeX

$$$$ \\sigma(a^n) = \\{ x^n : x \\in \\sigma(a) \\}. $$$$

Lean4

/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
convenience. -/
theorem map_pow_of_pos [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) : σ (a ^ n) = (· ^ n) '' σ a := by
  simpa only [aeval_X_pow, eval_X_pow] using
    map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos])

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