chore(Analysis/InnerProductSpace/Projection): deprecate module

j-loreaux · j-loreaux · commit a670d584af2b · 2025-08-14T12:32:10.000-05:00
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean
@@ -0,0 +1,7 @@
+import Mathlib.Analysis.InnerProductSpace.Projection.Basic
+import Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
+import Mathlib.Analysis.InnerProductSpace.Projection.Minimal
+import Mathlib.Analysis.InnerProductSpace.Projection.Reflection
+import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
+
+deprecated_module (since := "2025-08-08")
