toFinsupp_erase — Mathlib

English

Deleting the nth coefficient commutes with passing to finsupp: toFinsupp (p.erase n) = (p.toFinsupp).erase n.

Русский

Удаление n-го коэффициента commutec с переходом к finsupp: toFinsupp (p.erase n) = (p.toFinsupp).erase n.

LaTeX

$$$\\forall p:\\,R[X],\\forall n:\\,\\mathbb{N},\\ toFinsupp(p.erase n) = (toFinsupp(p)).erase n$$$

Lean4

@[simp]
theorem toFinsupp_erase (p : R[X]) (n : ℕ) : toFinsupp (p.erase n) = p.toFinsupp.erase n := by simp only [erase_def]

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