case hn
σ : Type u_1
τ : Type ?u.129675
R : Type u_2
S : Type ?u.129681
inst✝ : CommSemiring R
r : R
⊢ ∑ i in 0.support, ↑0 i = 0
σ : Type u_1
τ : Type ?u.129675
R : Type u_2
S : Type ?u.129681
inst✝ : CommSemiring R
r : R
⊢ IsHomogeneous (↑C r) 0
apply isHomogeneous_monomial
no goals
case hn
σ : Type u_1
τ : Type ?u.129675
R : Type u_2
S : Type ?u.129681
inst✝ : CommSemiring R
r : R
⊢ ∑ i in 0.support, ↑0 i = 0
simp only [Finsupp.zero_apply, Finset.sum_const_zero]