F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a, a ∈ Finset.erase s i ∧ eval (v j) (basisDivisor (v i) (v a)) = 0
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ eval (v j) (Lagrange.basis s v i) = 0
simp_rw [Lagrange.basis, eval_prod, prod_eq_zero_iff]
no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a, a ∈ Finset.erase s i ∧ eval (v j) (basisDivisor (v i) (v a)) = 0
exact ⟨j, ⟨mem_erase.mpr ⟨hij.symm, hj⟩, eval_basisDivisor_right⟩⟩