Commit 2020-09-02 15:51 57463fa4

View on Github →

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.

Estimated changes

Modified src/linear_algebra/affine_space/combination.lean

added theorem finset.affine_combination_map

added theorem finset.centroid_eq_affine_combination_fintype

added theorem finset.centroid_insert_singleton

added theorem finset.centroid_insert_singleton_fin

added theorem finset.centroid_map

added def finset.centroid_weights_indicator

added theorem finset.centroid_weights_indicator_def

added theorem finset.sum_centroid_weights_indicator

added theorem finset.sum_centroid_weights_indicator_eq_one_of_card_eq_add_one

added theorem finset.sum_centroid_weights_indicator_eq_one_of_card_ne_zero

added theorem finset.sum_centroid_weights_indicator_eq_one_of_nonempty

added theorem finset.weighted_vsub_map

added theorem finset.weighted_vsub_of_point_map

Modified src/linear_algebra/affine_space/finite_dimensional.lean

Modified src/linear_algebra/affine_space/independent.lean

added theorem affine.simplex.centroid_eq_iff

added theorem affine.simplex.face_centroid_eq_centroid

added theorem affine.simplex.face_centroid_eq_iff

added theorem affine.simplex.range_face_points

added theorem affine_independent_of_ne