Commit 2025-11-14 11:51 ef910756
View on Github →feat(Geometry/Euclidean/Projection): orthogonalProjectionSpan_congr (#31055)
Add a congruence lemma for orthogonalProjectionSpan applied to two simplices with the same set of vertices, analogous to and proved using orthogonalProjection_congr, and a variant
orthogonalProjectionSpan_reindex.