mathlib3

ab845455 - feat(linear_algebra/affine_space/finite_dimensional): collinearity and spans of two points (#17635)

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).