feat: port Analysis.Calculus.ContDiffDef (#4256)

Co-authored-by: @semorrison
leanprover-community · Jun 1, 2023 · 622fd5f · 622fd5f
1 parent bc20bc9
commit 622fd5f
Show file tree

Hide file tree

Showing 4 changed files with 1,704 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -416,6 +416,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
 import Mathlib.Analysis.BoxIntegral.Partition.Tagged
 import Mathlib.Analysis.Calculus.Conformal.InnerProduct
 import Mathlib.Analysis.Calculus.Conformal.NormedSpace
+import Mathlib.Analysis.Calculus.ContDiffDef
 import Mathlib.Analysis.Calculus.Darboux
 import Mathlib.Analysis.Calculus.Deriv.Add
 import Mathlib.Analysis.Calculus.Deriv.Basic