mathlib
mathlib copied to clipboard
Published
20 hours ago •
leanprover-community
leanprover-community
chore(data/polynomial/derivative): merge iterated_deriv.lean into derivative.lean
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.
I only discovered this as I was about to add the lemmas from #15954, of which a number already existed here - and I would have found them earlier if they had been with the other results about iterate_derivative in derivative.lean.
