Commit 2025-04-26 15:45 cb0f568c

refactor(Geometry/Euclidean/Projection): split out orthogonal projections (#24389) Split the definitions and lemmas about orthogonal projections from Mathlib.Geometry.Euclidean.Basic (plus some pieces in Mathlib.Geometry.Euclidean.Circumcenter) into a separate file Mathlib.Geometry.Euclidean.Projection. No definitions, statements or proofs are changed, just moved from one place to another (plus shake, plus fixing up the results of shake including import removals that worked but weren't pointed out by shake).