Commit 2025-07-27 16:19 d68f3de2
View on Github →chore(Analysis/InnerProductSpace/GramSchmidtOrtho): change definition to use U.starProjection x instead of (U.orthogonalProjection x : E) (#27334)
chore(Analysis/InnerProductSpace/GramSchmidtOrtho): change definition to use U.starProjection x instead of (U.orthogonalProjection x : E) (#27334)