Commit 2023-05-13 18:07 e3fb8404

chore(analysis/calculus/fderiv): split huge file into many pieces (#18995) Splits analysis/calculus/fderiv.lean into many subfiles. The file was already structured into well-organized sections. Small sections that fit well-together contentwise end up in a single file. Larger sections get their own file. The order of the sections changed a bit (to the extent that it still makes sense to say that they are ordered, after the split). But none of the sections were split into subsections.