Commit 2025-08-07 22:00 db788924

View on Github →

chore: move Polynomial.eval_map_algebraMap (#27959) This lemma is unrelated to IsScalarTower. It should not be placed in RingTheory.Polynomial.Tower.

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.eval_map_algebraMap

Modified Mathlib/Dynamics/Newton.lean

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

Modified Mathlib/RingTheory/Polynomial/Tower.lean

deleted theorem Polynomial.eval_map_algebraMap