Theorems · Definition · geometry
Finset.centroidWeights
(k : Type u_1) → [DivisionRing k] → {ι : Type u_4} → Finset ι → ι → kThe weights for the centroid of some points.
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.cardproof · cited by 2,327
- DivisionRingstatement and proof · cited by 1,062
Cited by29
Results whose statement or proof uses this declaration.
- Finset.centroidproof · cited by 45
- Finset.sum_centroidWeights_eq_one_of_nonemptystatement · cited by 8
- Finset.centroidWeightsIndicatorproof · cited by 7
- Finset.sum_centroidWeights_eq_one_of_card_ne_zerostatement · cited by 6
- Affine.Simplex.centroid_eq_affineCombinationstatement · cited by 5
- Affine.Simplex.centroid_vsub_eqproof · cited by 4
- Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenterproof · cited by 3
- Affine.Simplex.centroid_mapproof · cited by 3
- Finset.centroid_defstatement · cited by 3
- Affine.Simplex.faceOppositeCentroid_mapproof · cited by 3
- Finset.sum_centroidWeightsIndicatorstatement and proof · cited by 3
- Affine.Simplex.mongePoint_reindexproof · cited by 2