no goals
k : Type u_2
V : Type u_3
P : Type ?u.361200
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι✝ : Type ?u.361850
ι : Type u_1
p : ι → V
s : Finset ι
w : ι → k
hw : ∑ i in s, w i = 0
⊢ (↑(Finset.weightedVSub s p) w = 0 → ∀ (i : ι), i ∈ s → w i = 0) ↔ ∑ e in s, w e • p e = 0 → ∀ (e : ι), e ∈ s → w e = 0
simp [s.weightedVSub_eq_linear_combination hw]