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.