Commit 2025-08-12 02:14 a820a089

View on Github →

refactor(LinearAlgebra/AffineSpace/Combination) move centroid defintion to LinearAlgebra.AffineSpace.Centroid (#27919) This PR is the second step in the migration and split; see discussion in #27881

Move centroid related material from LinearAlgebra.AffineSpace.Combination to a new file LinearAlgebra.AffineSpace.Centroid
No changes or additions to any theorems, definitions, or proofs.
Added docstrings for the new file: LinearAlgebra.AffineSpace.Centroid
Fix the imports in LinearAlgebra.AffineSpace.Basis and LinearAlgebra.AffineSpace.Simplex.Centroid

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

Created Mathlib/LinearAlgebra/AffineSpace/Centroid.lean

added def Finset.centroid

added def Finset.centroidWeights

added def Finset.centroidWeightsIndicator

added theorem Finset.centroidWeightsIndicator_def

added theorem Finset.centroidWeights_apply

added theorem Finset.centroidWeights_eq_const

added theorem Finset.centroid_def

added theorem Finset.centroid_eq_affineCombination_fintype

added theorem Finset.centroid_eq_centroid_image_of_inj_on

added theorem Finset.centroid_eq_of_inj_on_of_image_eq

added theorem Finset.centroid_map

added theorem Finset.centroid_pair

added theorem Finset.centroid_pair_fin

added theorem Finset.centroid_singleton

added theorem Finset.centroid_univ

added theorem Finset.sum_centroidWeightsIndicator

added theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one

added theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero

added theorem Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty

added theorem Finset.sum_centroidWeights_eq_one_of_card_eq_add_one

added theorem Finset.sum_centroidWeights_eq_one_of_card_ne_zero

added theorem Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero

added theorem Finset.sum_centroidWeights_eq_one_of_nonempty

added theorem centroid_mem_affineSpan_of_card_eq_add_one

added theorem centroid_mem_affineSpan_of_card_ne_zero

added theorem centroid_mem_affineSpan_of_cast_card_ne_zero

added theorem centroid_mem_affineSpan_of_nonempty

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

deleted def Finset.centroid

deleted def Finset.centroidWeights

deleted def Finset.centroidWeightsIndicator

deleted theorem Finset.centroidWeightsIndicator_def

deleted theorem Finset.centroidWeights_apply

deleted theorem Finset.centroidWeights_eq_const

deleted theorem Finset.centroid_def

deleted theorem Finset.centroid_eq_affineCombination_fintype

deleted theorem Finset.centroid_eq_centroid_image_of_inj_on

deleted theorem Finset.centroid_eq_of_inj_on_of_image_eq

deleted theorem Finset.centroid_map

deleted theorem Finset.centroid_pair

deleted theorem Finset.centroid_pair_fin

deleted theorem Finset.centroid_singleton

deleted theorem Finset.centroid_univ

deleted theorem Finset.sum_centroidWeightsIndicator

deleted theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one

deleted theorem Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero

deleted theorem Finset.sum_centroidWeightsIndicator_eq_one_of_nonempty

deleted theorem Finset.sum_centroidWeights_eq_one_of_card_eq_add_one

deleted theorem Finset.sum_centroidWeights_eq_one_of_card_ne_zero

deleted theorem Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero

deleted theorem Finset.sum_centroidWeights_eq_one_of_nonempty

deleted theorem centroid_mem_affineSpan_of_card_eq_add_one

deleted theorem centroid_mem_affineSpan_of_card_ne_zero

deleted theorem centroid_mem_affineSpan_of_cast_card_ne_zero

deleted theorem centroid_mem_affineSpan_of_nonempty

Modified Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean