Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-22 11:57 46a88944

View on Github →

feat(linear_algebra/affine_space): affine combinations for finsets (#3122) Extend the definitions of affine combinations over a fintype to the case of sums over a finset of an arbitrary index type (which is appropriate for use cases such as affine independence of a possibly infinite family of points). Also change to have only bundled versions of weighted_vsub_of_point and weighted_vsub, following review, so avoiding duplicating parts of linear_map API.

Estimated changes