feat: port Analysis.InnerProductSpace.GramSchmidtOrtho (#4473)

leanprover-community · May 30, 2023 · 56e4133 · 56e4133
1 parent c57f43b
commit 56e4133
Show file tree

Hide file tree

Showing 2 changed files with 411 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -490,6 +490,7 @@ import Mathlib.Analysis.Hofer
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
 import Mathlib.Analysis.InnerProductSpace.Dual
+import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 import Mathlib.Analysis.InnerProductSpace.LaxMilgram
 import Mathlib.Analysis.InnerProductSpace.Orthogonal
 import Mathlib.Analysis.InnerProductSpace.PiL2