support_erase — Mathlib

English

The support of a polynomial after erasing the nth term equals the original support with n removed: supp(p.erase n) = supp(p) \\\\ {n}.

Русский

Опорa многочлена после стирания n-го члена равна исходной опоре с удалением n: supp(p.erase n) = supp(p) \\ {n}.

LaTeX

$$$\\operatorname{support}(p.erase n) = (\\operatorname{support}(p)).erase n$$$

Lean4

@[simp]
theorem support_erase (p : R[X]) (n : ℕ) : support (p.erase n) = (support p).erase n := by
  simp only [support, erase_def, Finsupp.support_erase]

Похожие утверждения