Commit 2022-02-24 11:57 b8b1b578

chore(geometry/euclidean): split repetitive proof (#12209) This PR is part of the subobject refactor #11545, fixing a timeout caused by some expensive defeq checks. I introduce a new definition simplex.orthogonal_projection_span s := orthogonal_projection (affine_span ℝ (set.range s.points)), and extract a couple of its properties from (repetitive) parts of proofs in circumcenter.lean, especially eq_or_eq_reflection_of_dist_eq. This makes the latter proof noticeably faster, especially after commit #11750.