English
The operation p.update n a replaces the nth coefficient of p by a; as a notation, it is (p.update n a) = ofFinsupp (p.toFinsupp.update n a). If a = 0 this coincides with p.erase n; more generally, if n is beyond the current degree and a ≠ 0, the degree may rise to n.
Русский
Операция p.update n a заменяет коэффициент при n на a; обозначение: (p.update n a) = ofFinsupp (p.toFinsupp.update n a). Если a = 0, то это равно p.erase n; если n превышает текущую степень и a ≠ 0, степень может стать равной n.
LaTeX
$$$p.update(n,a) = \\text{ofFinsupp}(p.toFinsupp.update(n,a))$$$
Lean4
@[simp]
theorem erase_zero (n : ℕ) : (0 : R[X]).erase n = 0 :=
toFinsupp_injective <| by simp
