English
The coefficient function of the updated element is obtained by updating the original coefficient function at the chosen index. In other words, for every index a', the coefficient of a' in f.update a b equals b if a' = a, and equals f.coeff(a') otherwise.
Русский
Коэффициентная функция обновленного элемента получается путём обновления исходной коэффициентной функции в выбранном индексе. То есть для каждого индекса a' коэффициент f.update a b при a' равен b, если a' = a, и равен f.coeff a' в противном случае.
LaTeX
$$$\\big( (f.update\\ a\\ b) \\big).\\text{coeff} = \\text{Function.update}( f.\\text{coeff} )\\ a\\ b$$$
Lean4
theorem coeff_update [DecidableEq α] : (f.update a b).coeff = Function.update f.coeff a b :=
by
simp only [coeff, update, Finsupp.update, Finsupp.coe_mk]
congr!
