mathlib3

593b1bb5 - feat(linear_algebra/affine_space): lemmas on affine spans (#3453)

feat(linear_algebra/affine_space): lemmas on affine spans (#3453) Add more lemmas on affine spans; in particular, that the points in an `affine_span` are exactly the `affine_combination`s where the sum of weights equals 1, provided the underlying ring is nontrivial.