mathlib3

6c5959aa - feat(linear_algebra/affine_space/finite_dimensional): more affine independence / collinearity lemmas (#17643)

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