Commit 2026-06-05 08:51 94a13dfd

View on Github →

feat(Algebra/Polynomial): leading coefficient of derivative (#40173) Also fix a few names and variable implicitness and create a section for the lemmas that require IsAddTorsionFree R. From RealRooted

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

added theorem WithBot.unbotD_natCast

added theorem WithBot.unbotD_ofNat

Modified Mathlib/Algebra/Polynomial/Derivative.lean

added theorem Polynomial.degree_derivative

modified theorem Polynomial.degree_derivative_eq

added theorem Polynomial.derivative_eq_zero

added theorem Polynomial.derivative_ne_zero

modified theorem Polynomial.eq_C_of_derivative_eq_zero

added theorem Polynomial.leadingCoeff_derivative

modified theorem Polynomial.mem_support_derivative

added theorem Polynomial.natDegree_derivative

deleted theorem Polynomial.natDegree_eq_zero_of_derivative_eq_zero

Modified Mathlib/FieldTheory/Differential/Basic.lean

Modified Mathlib/FieldTheory/Separable.lean