Theorems · Theorem · field theory

spectrum.map_polynomial_aeval_of_degree_pos

∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A)
  (p : Polynomial 𝕜),
  0 < p.degree → spectrum 𝕜 ((Polynomial.aeval a) p) = (fun x => Polynomial.eval x p) '' spectrum 𝕜 a

The spectral mapping theorem for polynomials. Note: the assumption degree p > 0 is necessary in case σ a = ∅, for then the left-hand side is ∅ and the right-hand side, assuming [Nontrivial A], is {k} where p = Polynomial.C k.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Spectrum

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebraIsAlgClosed