no goals
k : Type u_4
V : Type u_5
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_2
s : Finset ι
ι₂ : Type u_1
s₂ : Finset ι₂
e : ι₂ ↪ ι
p : ι → P
⊢ centroid k (map e s₂) p = centroid k s₂ (p ∘ ↑e)
simp [centroid_def, affineCombination_map, centroidWeights]