Commit 2020-10-05 07:39 1c8bb422

feat(linear_algebra/affine_space/finite_dimensional): more lemmas (#4389) Add more lemmas concerning dimensions of affine spans of finite families of points. In particular, various forms of the lemma that n + 1 points are affinely independent if and only if their vector_span has dimension n (or equivalently, at least n). With suitable definitions, this is equivalent to saying that three points are affinely independent or collinear, four are affinely independent or coplanar, etc., thus preparing for giving a definition of collinear (for any set of points in an affine space for a vector space) in terms of dimension and proving some basic properties of it including relating it to affine independence.