feat: port Analysis.Calculus.Implicit (#4665)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
leanprover-community · Jun 22, 2023 · 3c283ad · 3c283ad
1 parent c061be5
commit 3c283ad
Show file tree

Hide file tree

Showing 2 changed files with 489 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -518,6 +518,7 @@ import Mathlib.Analysis.Calculus.FDerivAnalytic
 import Mathlib.Analysis.Calculus.FDerivMeasurable
 import Mathlib.Analysis.Calculus.FDerivSymmetric
 import Mathlib.Analysis.Calculus.FormalMultilinearSeries
+import Mathlib.Analysis.Calculus.Implicit
 import Mathlib.Analysis.Calculus.Inverse
 import Mathlib.Analysis.Calculus.IteratedDeriv
 import Mathlib.Analysis.Calculus.LHopital