Commit 2025-10-24 22:09 97d68c42

View on Github →

chore: deprecate duplicate Polynomial.monic_of_degree_le_of_coeff_eq_one (#30865)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Degree/Operations.lean

added theorem Polynomial.monic_of_degree_le

deleted theorem Polynomial.monic_of_degree_le_of_coeff_eq_one

Modified Mathlib/Algebra/Polynomial/Monic.lean

deleted theorem Polynomial.monic_of_degree_le

Modified Mathlib/RingTheory/Polynomial/IntegralNormalization.lean