Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes