R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ Finsupp.erase n 0 = 0
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (erase n 0).toFinsupp = 0.toFinsupp
simp
no goals
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ Finsupp.erase n 0 = 0
exact Finsupp.erase_zero n