Commit 2022-03-21 05:51 69d3d16b

View on Github →

feat(polynomial/derivative): tidy+new theorems (#12833) Adds iterate_derivative_eq_zero and strengthens other results. New theorems: iterate_derivative_eq_zero, nat_degree_derivative_le Deleted: derivative_lhom - it is one already. Misc: Turn a docstring into a comment Everything else only got moved around + golfed, in order to weaken assumptions.

Estimated changes

Modified src/data/polynomial/derivative.lean

deleted def polynomial.derivative_lhom

deleted theorem polynomial.derivative_lhom_coe

modified theorem polynomial.derivative_neg

modified theorem polynomial.derivative_sub

added theorem polynomial.iterate_derivative_eq_zero

modified theorem polynomial.iterate_derivative_neg

modified theorem polynomial.iterate_derivative_sub

added theorem polynomial.nat_degree_derivative_le

modified theorem polynomial.nat_degree_eq_zero_of_derivative_eq_zero

Modified src/ring_theory/polynomial/bernstein.lean