feat: port Analysis.Calculus.Fderiv.Prod (#4208)

leanprover-community · May 22, 2023 · c851d27 · c851d27
1 parent 314e4d6
commit c851d27
Show file tree

Hide file tree

Showing 2 changed files with 470 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -382,6 +382,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Tagged
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Comp
 import Mathlib.Analysis.Calculus.FDeriv.Linear
+import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 import Mathlib.Analysis.Calculus.TangentCone
 import Mathlib.Analysis.Complex.Basic