English
For any polynomial p and any degree n, the polynomial p.erase n is obtained from p by removing the X^n-term, i.e. the coefficient of X^n is set to zero and all other coefficients remain unchanged.
Русский
Для любого многочлена p и степени n полином p.erase n получается из p удалением термина X^n: коэффициент при X^n становится нулём, все другие коэффициенты не меняются.
LaTeX
$$$\\forall p:\\,R[X],\\forall n:\\,\\mathbb{N},\\ p.erase\\ n = \\text{polynomial obtained from }p\\ by\\ setting\\ coeff\\ at\\ n\\ to\\ 0$$$
Lean4
/-- `erase p n` is the polynomial `p` in which the `X^n` term has been erased. -/
def erase :=
val_proj @wrapped✝.{}
