chore(analysis/calculus/fderiv): split huge file into many pieces (#1…

…8995)

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>

src/analysis/box_integral/divergence_theorem.lean

@@ -5,7 +5,10 @@ Authors: Yury Kudryashov
 -/
 import analysis.box_integral.basic
 import analysis.box_integral.partition.additive
-import analysis.calculus.fderiv.basic
+import analysis.calculus.fderiv.add
+import analysis.calculus.fderiv.mul
+import analysis.calculus.fderiv.equiv
+import analysis.calculus.fderiv.restrict_scalars
 
 /-!
 # Divergence integral for Henstock-Kurzweil integral

src/analysis/calculus/conformal/normed_space.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang
 -/
 import analysis.normed_space.conformal_linear_map
-import analysis.calculus.fderiv.basic
+import analysis.calculus.fderiv.add
+import analysis.calculus.fderiv.mul
+import analysis.calculus.fderiv.equiv
+import analysis.calculus.fderiv.restrict_scalars
 
 /-!
 # Conformal Maps

src/analysis/calculus/cont_diff_def.lean

@@ -3,7 +3,10 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import analysis.calculus.fderiv.basic
+import analysis.calculus.fderiv.add
+import analysis.calculus.fderiv.mul
+import analysis.calculus.fderiv.equiv
+import analysis.calculus.fderiv.restrict_scalars
 import analysis.calculus.formal_multilinear_series
 
 /-!

src/analysis/calculus/deriv.lean

@@ -3,7 +3,10 @@ Copyright (c) 2019 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sébastien Gouëzel
 -/
-import analysis.calculus.fderiv.basic
+import analysis.calculus.fderiv.add
+import analysis.calculus.fderiv.mul
+import analysis.calculus.fderiv.equiv
+import analysis.calculus.fderiv.restrict_scalars
 import data.polynomial.algebra_map
 import data.polynomial.derivative
 import linear_algebra.affine_space.slope