feat: port Analysis.Calculus.FDeriv.Mul (#4241)

leanprover-community · May 25, 2023 · 75e8a74 · 75e8a74
1 parent 2785e7d
commit 75e8a74
Show file tree

Hide file tree

Showing 2 changed files with 541 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -405,6 +405,7 @@ import Mathlib.Analysis.Calculus.FDeriv.Bilinear
 import Mathlib.Analysis.Calculus.FDeriv.Comp
 import Mathlib.Analysis.Calculus.FDeriv.Equiv
 import Mathlib.Analysis.Calculus.FDeriv.Linear
+import Mathlib.Analysis.Calculus.FDeriv.Mul
 import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 import Mathlib.Analysis.Calculus.FDeriv.Star