Commit 2023-09-20 11:42 4026e6f8

View on Github →

feat: some theorems about iterated polynomial derivatives (#7274)

Estimated changes

Modified Mathlib/Data/Polynomial/Derivative.lean

added theorem Polynomial.coeff_iterate_derivative

deleted theorem Polynomial.coeff_iterate_derivative_as_prod_Ico

deleted theorem Polynomial.coeff_iterate_derivative_as_prod_range

added theorem Polynomial.natDegree_iterate_derivative