mathlib3

8f02ad2f - feat(geometry/euclidean): orthogonal projection (#3662)

feat(geometry/euclidean): orthogonal projection (#3662) Define orthogonal projection onto an affine subspace of a Euclidean affine space, and prove some basic lemmas about it. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>