Commit 2025-08-08 08:19 4b30dc19

chore(Analysis/InnerProductSpace/Projection): split file (#27851) Splitting long file Analysis.InnerProductSpace.Projection:

• Projection/Minimal: contains the Hilbert projection theorem and minimizer characterization.
• Projection/Basic: contains the definitions for HasOrthogonalProjection, othogonalProjection, starProjection and pretty much everything concerning those.
• Projection/Reflection: everything about Submodule.reflection.
• Projection/Submodule: stuff like K ⊔ Kᗮ = ⊤ for when K admits an orthogonal projection.
• Projection/FiniteDimensional: stuff about orthogonal projections on finite-dimensional spaces (but also some lemmas that doesn't use FiniteDimensional).