Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-14 08:03 51608f4a

View on Github →

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.

Estimated changes