Commit 2022-02-24 11:57 b8b1b578
View on Github →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.