mathlib

f651d75e - chore(data/polynomial/derivative): merge iterated_deriv.lean into derivative.lean (#16022)

chore(data/polynomial/derivative): merge iterated_deriv.lean into derivative.lean (#16022) iterated_deriv.lean was not used anywhere, and derivative.lean already had independent variants of several of the lemmas there, without the `iterated_deriv` indirecion. It seems better to consolidate these results.