Commit 2020-10-05 11:39 ca269b44
View on Github →feat(linear_algebra/affine_space/finite_dimensional): collinearity (#4433)
Define collinearity of a set of points in an affine space for a vector
space (as meaning the vector_span has dimension at most 1), and
prove some basic lemmas about it, leading to three points being
collinear if and only if they are not affinely independent.