no goals
k : Type u_1
V : Type ?u.465735
P : Type ?u.465738
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type ?u.466257
s₂ : Finset ι₂
h : ↑(card s) ≠ 0
⊢ ∑ i in s, centroidWeights k s i = 1
simp [h]