Commit 2022-08-18 17:58 f651d75e

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.