Commit 2025-10-13 07:43 4e9ce78e

View on Github →

chore: Polynomial.eval_X_pow (#30446) This is of course just eval_pow + eval_X, but I believe it appears commonly enough to warrant its own shortcut.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

added theorem Polynomial.eval_X_pow

Modified Mathlib/Algebra/Polynomial/GroupRingAction.lean

Modified Mathlib/Algebra/Polynomial/UnitTrinomial.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Modified Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

Modified Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/RingTheory/LittleWedderburn.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean

Modified Mathlib/RingTheory/RootsOfUnity/Minpoly.lean