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

leanprover-community · Jul 13, 2023 · 625a3a6 · 625a3a6
1 parent 906f722
commit 625a3a6
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