no goals
k : Type u_2
V : Type ?u.413734
P : Type ?u.413737
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.414393
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ affineCombinationSingleWeights k i j = 0
simp [affineCombinationSingleWeights, h]