fderiv): move large file to dedicated subfolder, prepare for split (#19007)

Commit

2 years ago

chore(analysis/calculus/fderiv): move large file to dedicated subfolder, prepare for split (#19007) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

jcommelin

Parents

403190b5

mathlib 58537299 - chore(analysis/calculus/fderiv): move large file to dedicated subfolder, prepare for split (#19007)

mathlib
58537299 - chore(analysis/calculus/fderiv): move large file to dedicated subfolder, prepare for split (#19007)