feat: port Analysis.InnerProductSpace.Calculus (#4659)

leanprover-community · Jun 5, 2023 · d27c625 · d27c625
1 parent f30dbfc
commit d27c625
Show file tree

Hide file tree

Showing 2 changed files with 393 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -521,6 +521,7 @@ import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.Hofer
 import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.InnerProductSpace.Calculus
 import Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho