Commit 2025-10-26 13:57 5cdb67dd

View on Github →

chore: deprecate duplicate Polynomial.Monic.natDegree_eq_zero_iff_eq_one (#30922)

Estimated changes

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

Modified Mathlib/Algebra/Polynomial/Monic.lean

deleted theorem Polynomial.Monic.natDegree_eq_zero_iff_eq_one

Modified Mathlib/Topology/Algebra/Polynomial.lean