Commit 2022-12-04 14:17 6c5959aa

feat(linear_algebra/affine_space/finite_dimensional): more affine independence / collinearity lemmas (#17643) Add more variants of affine_independent_iff_not_collinear and collinear_iff_not_affine_independent: versions where the three points are listed explicitly using ![] and in the set rather than using set.range, and versions where three distinct indices are given and the set is expressed as {p i₁, p i₂, p i₃} (the latter are of use when proving geometrical results involving triangles, which are stated with indices like that to make it convenient to apply them at any point of the triangle).