mathlib

797177c3 - feat(linear_algebra/affine_space): affine combinations of points (#2979)

feat(linear_algebra/affine_space): affine combinations of points (#2979) Some basic definitions and lemmas related to affine combinations of points, in preparation for defining barycentric coordinates for use in geometry. This version for sums over a `fintype` is probably the most convenient for geometrical uses (where the type will be `fin 3` in the case of a triangle, or more generally `fin (n + 1)` for an n-simplex), but other use cases may find that `finset` or `finsupp` versions of these definitions are of use as well. The definition `weighted_vsub` is expected to be used with weights that sum to zero, and the definition `affine_combination` is expected to be used with weights that sum to 1, but such a hypothesis is only specified for lemmas that need it rather than for those definitions. I expect that most nontrivial geometric uses of barycentric coordinates will need to prove such a hypothesis at some point, but that it will still be more convenient not to need to pass it to all the definitions and trivial lemmas. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>