k : Type u_2
V : Type ?u.425950
P : Type ?u.425953
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.426609
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ x in s, affineCombinationSingleWeights k i x - ∑ x in s, affineCombinationSingleWeights k j x = 0
k : Type u_2
V : Type ?u.425950
P : Type ?u.425953
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.426609
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ t in s, weightedVSubVSubWeights k i j t = 0
simp_rw [weightedVSubVSubWeights, Pi.sub_apply, sum_sub_distrib]
no goals
k : Type u_2
V : Type ?u.425950
P : Type ?u.425953
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_1
s : Finset ι
ι₂ : Type ?u.426609
s₂ : Finset ι₂
inst✝ : DecidableEq ι
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ ∑ x in s, affineCombinationSingleWeights k i x - ∑ x in s, affineCombinationSingleWeights k j x = 0
simp [hi, hj]