Commit 2022-12-06 20:53 ab845455

feat(linear_algebra/affine_space/finite_dimensional): collinearity and spans of two points (#17635) Add a series of lemmas that if some points are in the line through two points, the set of all points involved, and subsets thereof, are themselves collinear (obviously any number of such variations could be written; these are ones I've found of use in practice).