Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-29 09:36 545c2655

View on Github →

feat(data/polynomial/derivative): if p is a polynomial, then p.derivative.nat_degree ≤ p.nat_degree - 1 (#12948) I also golfed the proof that p.derivative.nat_degree ≤ p.nat_degree.

Estimated changes