Commit 2025-07-11 01:56 b821f6e3

feat(Analysis/InnerProductSpace/Projection): define Submodule.starProjection (#25958) This defines Submodule.starProjection, the orthogonal projection onto a subspace as a map from the full space to itself, as opposed to Submodule.orthogonalProjection, which maps into the subtype. This version is important as it satisfies IsStarProjection. Lemma: an operator is a star projection iff it is an orthogonal projection (i.e., IsStarProjection p iff p = (LinearMap.range p).starProjection).