Commit 2020-08-15 20:41 c9bf6f24

feat(linear_algebra/affine_space/independent): affinely independent sets (#3794) Prove variants of affine_independent_iff_linear_independent_vsub that relate affine independence for a set of points (as opposed to an indexed family of points) to linear independence for a set of vectors, so facilitating linking to results such as exists_subset_is_basis expressed in terms of linearly independent sets of vectors. There are two variants, depending on which of the set of points or the set of vectors is given as a hypothesis. Thus, applying exists_subset_is_basis, deduce that if k is a field, any affinely independent set of points can be extended to such a set that spans the whole space. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear.20suffering