English
The derivative distributes as a sum of nodal polynomials with each node removed in turn.
Русский
Производная нодального полинома равна сумме по i∈s от nodal(s\\{i}, v).
LaTeX
$$$ \\frac{d}{dX}(\\operatorname{nodal}(s,v)) = \\sum_{i\\in s} \\operatorname{nodal}(s\\setminus i, v). $$$
Lean4
theorem derivative_nodal [DecidableEq ι] : derivative (nodal s v) = ∑ i ∈ s, nodal (s.erase i) v :=
by
refine s.induction_on ?_ fun i t hit IH => ?_
· rw [nodal_empty, derivative_one, sum_empty]
· rw [nodal_insert_eq_nodal hit, derivative_mul, IH, derivative_sub, derivative_X, derivative_C, sub_zero, one_mul,
sum_insert hit, mul_sum, erase_insert hit, add_right_inj]
refine sum_congr rfl fun j hjt => ?_
rw [t.erase_insert_of_ne (ne_of_mem_of_not_mem hjt hit).symm, nodal_insert_eq_nodal (mem_of_mem_erase.mt hit)]
