English
The support of p.update n a is obtained by updating the support of p: if a ≠ 0, n is inserted into the support; if a = 0, n is erased from the support.
Русский
Опора (множество индексов с ненулевыми коэффициентами) многочлена после обновления: если a ≠ 0, добавляем n в опору; если a = 0, удаляем n из опоры.
LaTeX
$$$\\operatorname{support}(p.update n a) = \\begin{cases} \\operatorname{support}(p) \\setminus \\{n\\}, & a=0, \\\\ \\operatorname{support}(p) \\cup \\{n\\}, & a\\neq 0. \\end{cases}$$$
Lean4
theorem support_update (p : R[X]) (n : ℕ) (a : R) [Decidable (a = 0)] :
support (p.update n a) = if a = 0 then p.support.erase n else insert n p.support := by
classical
simp only [support, update, Finsupp.support_update]
congr
