English
Let f be a Skew Monoid Algebra element, and let a be an index and b a coefficient. Then updating f at a by b changes the support exactly by inserting a when b ≠ 0, and by removing a when b = 0. Equivalently, the new support is obtained from the old support by deleting a if b = 0, or by inserting a into the old support if b ≠ 0.
Русский
Пусть f — элемент SkewMonoidAlgebra, пусть a — индекс, а b — коэффициент. Обновление f в позиции a на значение b изменяет опору ровно так, что если b = 0, то из опоры удаляется a; если b ≠ 0, то в опоре добавляется a. Эквивалентно, новая опора получается из старой путём удаления a при b = 0 или добавления a при b ≠ 0.
LaTeX
$$$\\operatorname{supp}(f.update\\ a\\ b) = \\begin{cases} \\operatorname{supp}(f) \\setminus \\{a\\}, & b = 0, \\\\ \\operatorname{supp}(f) \\cup \\{a\\}, & b \\neq 0. \\end{cases}$$$
Lean4
theorem support_update [DecidableEq α] [DecidableEq M] :
support (f.update a b) = if b = 0 then f.support.erase a else insert a f.support := by
aesop (add norm [update, Finsupp.support_update_ne_zero])
