Theorems · Theorem · field theory

spectrum.map_polynomial_aeval_of_nonempty

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

In this version of the spectral mapping theorem, we assume the spectrum is nonempty instead of assuming the degree of the polynomial is positive.

Defined in

Mathlib.FieldTheory.IsAlgClosed.Spectrum

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebraIsAlgClosed