Theorems · Theorem · field theory

spectrum.pow_image_subset

∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (n : ℕ),
  (fun x => x ^ n) '' spectrum 𝕜 a ⊆ spectrum 𝕜 (a ^ n)

A specialization of spectrum.subset_polynomial_aeval to monic monomials for convenience.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Spectrum

Cited by

1 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingAlgebra