derivative): if `p` is a polynomial, then `p.derivative.nat_degree ≤ p.nat_degree - 1` (#12948)

Commit

3 years ago

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`.

Author

adomani

Parents

4bf4d9df

mathlib3 545c2655 - feat(data/polynomial/derivative): if `p` is a polynomial, then `p.derivative.nat_degree ≤ p.nat_degree - 1` (#12948)

mathlib3
545c2655 - feat(data/polynomial/derivative): if `p` is a polynomial, then `p.derivative.nat_degree ≤ p.nat_degree - 1` (#12948)