feat: port Geometry.Manifold.ContMdiffMfderiv (#5496)

leanprover-community · Aug 14, 2023 · 1dc3ab3 · 1dc3ab3
1 parent f587581
commit 1dc3ab3
Show file tree

Hide file tree

Showing 3 changed files with 622 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1891,6 +1891,7 @@ import Mathlib.Geometry.Manifold.ChartedSpace
 import Mathlib.Geometry.Manifold.Complex
 import Mathlib.Geometry.Manifold.ConformalGroupoid
 import Mathlib.Geometry.Manifold.ContMDiff
+import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 import Mathlib.Geometry.Manifold.ContMDiffMap
 import Mathlib.Geometry.Manifold.DerivationBundle
 import Mathlib.Geometry.Manifold.Diffeomorph