Commit 2020-06-29 13:48 78beab4f
View on Github →feat(linear_algebra/affine_space): affine independence (#3140)
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.