pow_mem_pow — Mathlib

English

Let a be as above with (σ(a)).Nonempty. Then σ(a^n) = { x^n : x ∈ σ(a) } for any n ∈ ℕ. This is the nonempty-spectrum specialization of the polynomial spectral mapping theorem to monomials.

Русский

Пусть σ(a) непусто. Тогда σ(a^n) = { x^n : x ∈ σ(a) } для любого n ∈ ℕ. Это частный случай теоремы спектрального отображения для монономов.

LaTeX

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

Lean4

theorem pow_mem_pow (a : A) (n : ℕ) {k : 𝕜} (hk : k ∈ σ a) : k ^ n ∈ σ (a ^ n) :=
  pow_image_subset a n ⟨k, ⟨hk, rfl⟩⟩

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