feat: port Analysis.Calculus.FDeriv.Basic (#4132)

leanprover-community · May 21, 2023 · 2a3dcf0 · 2a3dcf0
1 parent 5e4ff03
commit 2a3dcf0
Show file tree

Hide file tree

Showing 2 changed files with 1,144 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -376,6 +376,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Basic
 import Mathlib.Analysis.BoxIntegral.Partition.Split
 import Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
 import Mathlib.Analysis.BoxIntegral.Partition.Tagged
+import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.TangentCone
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Complex.Circle