Commit 2026-06-09 00:16 495d64fd

View on Github →

feat(Algebra/Polynomial): lemmas about modByMonic (#37955)

Add various small lemmas about Polynomial.modByMonic
Remove unneccesary commutativity assumption on Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero by proving Polynomial.aeval_dvd

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.aeval_dvd

modified theorem Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero

Modified Mathlib/Algebra/Polynomial/Div.lean

added theorem Polynomial.dvd_modByMonic_iff_dvd

added theorem Polynomial.dvd_modByMonic_sub

added theorem Polynomial.modByMonic_self

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

Modified Mathlib/FieldTheory/Minpoly/Basic.lean

added theorem minpoly.aeval_modByMonic_minpoly

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/Polynomial/IsIntegral.lean