Commit 2020-08-17 09:11 626de475

feat(linear_algebra/affine_space/combination): centroid (#3825) Define the centroid of points in an affine space (given by an indexed family with a finset of the index type), when the underlying ring k is a division ring, and prove a few lemmas about cases where this does not involve division by zero. For example, the centroid of a triangle or simplex, although none of the definitions and lemmas here require affine independence so they are all stated more generally. (The sort of things that would be appropriate to state specifically for the case of a simplex would be e.g. defining medians and showing that the centroid is the intersection of any two medians.)