# Commit 2020-06-14 19:26 797177c3

View on Github →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.