F : Type u_2
inst✝ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
hi : i ∈ s
⊢ ∃ a, a ∈ s ∧ v i - v a = 0
F : Type u_2
inst✝ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
hi : i ∈ s
⊢ eval (v i) (nodal s v) = 0
rw [eval_nodal, prod_eq_zero_iff]
no goals
F : Type u_2
inst✝ : Field F
ι : Type u_1
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
hi : i ∈ s
⊢ ∃ a, a ∈ s ∧ v i - v a = 0
exact ⟨i, hi, sub_eq_zero_of_eq rfl⟩