mathlib3

51608f4a - feat(linear_algebra/affine_space,geometry/euclidean): simplex centers and order of points (#4116)

feat(linear_algebra/affine_space,geometry/euclidean): simplex centers and order of points (#4116) Add lemmas that the centroid of an injective indexed family of points does not depend on the indices of those points, only on the set of points in their image, and likewise that the centroid, circumcenter and Monge point of a simplex and thus the orthocenter of a triangle do not depend on the order in which the vertices are indexed by `fin (n + 1)`, only on the set of vertices.