feat: port Analysis.InnerProductSpace.Basic (#4280)

I had to add big `maxHeartbeats` increases into two places, but I haven't been able to improve the situation (it compiles though). This might need to be addressed before merging. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
leanprover-community · May 25, 2023 · fea3e4c · fea3e4c
1 parent a1c58a9
commit fea3e4c
Show file tree

Hide file tree

Showing 3 changed files with 2,369 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -452,6 +452,7 @@ import Mathlib.Analysis.Convex.StrictConvexSpace
 import Mathlib.Analysis.Convex.Topology
 import Mathlib.Analysis.Convex.Uniform
 import Mathlib.Analysis.Hofer
+import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.LocallyConvex.AbsConvex
 import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 import Mathlib.Analysis.LocallyConvex.Basic