[Merged by Bors] - feat(linear_algebra/affine_space): affine independence

[jsm28]

Define affine independent indexed families of points (in terms of no
nontrivial weighted_vsub in the family being zero), prove that a
family of at most one point is affine independent, and prove a family
of points is affine independent if and only if a corresponding family
of subtractions is linearly independent.

There are of course other equivalent descriptions of affine
independent families it will be useful to add later (that the affine
span of all proper subfamilies is smaller than the affine span of the
whole family, that each point is not in the affine span of the rest;
in the case of a family indexed by a fintype, that the dimension of
the affine span is one less than the cardinality). But I think the
definition and one equivalent formulation is a reasonable starting
point.

---

[PatrickMassot]

That proof seems too big. Are you sure you can't factor out a couple of useful lemmas?

[jsm28]

The lemmas I could find that seemed possibly relevant to more than just this proof were merged in #3124. The two directions of the lemma could of course be split into separate lemmas linear_independent_vsub_of_affine_independent and affine_independent_of_linear_independent_vsub, but while that might make it quicker for Lean to process, it wouldn't make the proof any simpler.

[PatrickMassot]

I'm sorry but I'm not convinced. I can't really believe you couldn't develop the theory of equiv.vadd_const and equiv.const_vadd to help here.

[semorrison]

@PatrickMassot --- maybe you can indicate what you'd like to see when you said "I can't really believe you couldn't develop the theory of equiv.vadd_const and equiv.const_vadd to help here."?

[jsm28]

I certainly couldn't see the relevance of equiv.vadd_const and equiv.const_vadd. The proof is all manipulations of sums and subtypes; I've split out eight lemmas about such manipulations (not counting to_additive variants separately), but that doesn't make the proof that much shorter as it's still necessary to set up hypotheses in the right form for using those lemmas.

[jcommelin]

You still went down from ~70 lines to ~50 lines. And all the new results will hopefully be useful in later developments, hence pay off in the long run.
(I haven't really reviewd the PR yet.)

[PatrickMassot]

I certainly couldn't see the relevance of equiv.vadd_const and equiv.const_vadd.

The statement is definitionaly equal to

affine_independent k V p ↔ linear_independent k (λ i : {x // x ≠ i1}, (vadd_const V (p i1)).symm $ p i)

How could it fail to be relevant? My question is: could you write lemmas about vadd_const that could prove this lemma. It seems to me that vadd_const is a central object in the theory, and I find it surprising that it's not use more. However I'm already very happy with your recent work. Anything that remove lines from a specialized proof to add them to big_operator is worth the trouble in my opinion.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs