mathlib
e3fb8404 - chore(analysis/calculus/fderiv): split huge file into many pieces (#18995)

Commit
2 years ago
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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading