no goals
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
⊢ (fun x => x ^ n) '' σ a ⊆ σ (a ^ n)
simpa only [eval_pow, eval_X, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])