simp only [homogenization, totalDegree_C, zero_tsub]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ homogenization i (C c) = C c
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i 0) (C c) = C c