mathlib

57463fa4 - feat(linear_algebra/affine_space): more lemmas (#3990)

feat(linear_algebra/affine_space): more lemmas (#3990) Add another batch of lemmas about affine spaces. These lemmas mostly relate to manipulating centroids and the relations between centroids of points given by different subsets of the index type.