simp [RingHom.iterate_map_zero, mul_zero, AddMonoidAlgebra.single_zero]
case h_zero
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a b c : R[X;φ]
⊢ ∀ (a : ℕ), (sum c.toFinsupp fun a₂ b₂ => single (a + a₂) (0 * (↑φ)^[a] b₂)) = 0
no goals