have : (0 : ι →₀ ℕ) i = 0 := by simp only [Finsupp.coe_zero, Pi.zero_apply]
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = (monomial (0 + Finsupp.single i 0)) c
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i 0)) c