convert isHomogeneous_C (R := R) _ _
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).IsHomogeneous (C r).totalDegree
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).totalDegree = 0