Commit 2026-03-02 13:09 11962c62

View on Github →

chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas (#31817)

Estimated changes

Modified Mathlib/Algebra/Polynomial/CoeffMem.lean

modified theorem Polynomial.idealSpan_range_update_divByMonic

Modified Mathlib/Algebra/Polynomial/Div.lean

modified theorem Polynomial.degree_divByMonic_lt

modified theorem Polynomial.eval₂_modByMonic_eq_self_of_root

modified theorem Polynomial.modByMonic_add_div

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Algebra/Polynomial/PartialFractions.lean

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

modified theorem Polynomial.aeval_modByMonic_eq_self_of_root

Modified Mathlib/Analysis/Polynomial/Basic.lean

Modified Mathlib/FieldTheory/Minpoly/Basic.lean

Modified Mathlib/FieldTheory/Minpoly/Field.lean

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

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

Modified Mathlib/RingTheory/Polynomial/Nilpotent.lean

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean

Modified Mathlib/RingTheory/Smooth/IntegralClosure.lean

Modified Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean

Modified Mathlib/RingTheory/ZariskisMainTheorem.lean