no goals
F : Type u_2
inst✝ : Field F
ι : Type u_1
s : Finset ι
v✝ : ι → F
i : ι
r : ι → F
x : F
v : ι → F
hi : i ∈ s
⊢ nodal s v = (X - ↑C (v i)) * ?m.392653 v hi
classical exact nodal_eq_mul_nodal_erase hi
no goals
F : Type u_2
inst✝ : Field F
ι : Type u_1
s : Finset ι
v✝ : ι → F
i : ι
r : ι → F
x : F
v : ι → F
hi : i ∈ s
⊢ nodal s v = (X - ↑C (v i)) * ?m.392653 v hi
exact nodal_eq_mul_nodal_erase hi