English
The erase operation agrees with the canonical decomposition of a polynomial into its finsupp representation: erasing the nth coefficient corresponds to erasing the nth entry in the finsupp that encodes the polynomial.
Русский
Операция стирания согласуется с каноническим разложением многочлена в представление через фунсипп: стирание коэффициента при n соответствует удалению n-го элемента в представлении через finsupp.
LaTeX
$$$\\text{erase}(n, p)\\ \text{is characterized by}\\ (\\text{erase}(n, p).toFinsupp = (p.toFinsupp).erase(n))$$$
Lean4
theorem erase_def : eta_helper Eq✝ @erase.{} @(delta% @definition✝) :=
by
intros
delta erase
rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
rfl
