case hn
σ : Type u_1
τ : Type ?u.153374
R : Type u_2
S : Type ?u.153380
inst✝ : CommSemiring R
i : σ
⊢ ∑ i_1 in (Finsupp.single i 1).support, ↑(Finsupp.single i 1) i_1 = 1
σ : Type u_1
τ : Type ?u.153374
R : Type u_2
S : Type ?u.153380
inst✝ : CommSemiring R
i : σ
⊢ IsHomogeneous (X i) 1
apply isHomogeneous_monomial
case hn
σ : Type u_1
τ : Type ?u.153374
R : Type u_2
S : Type ?u.153380
inst✝ : CommSemiring R
i : σ
⊢ ↑(Finsupp.single i 1) i = 1
case hn
σ : Type u_1
τ : Type ?u.153374
R : Type u_2
S : Type ?u.153380
inst✝ : CommSemiring R
i : σ
⊢ ∑ i_1 in (Finsupp.single i 1).support, ↑(Finsupp.single i 1) i_1 = 1
rw [Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton]
no goals
case hn
σ : Type u_1
τ : Type ?u.153374
R : Type u_2
S : Type ?u.153380
inst✝ : CommSemiring R
i : σ
⊢ ↑(Finsupp.single i 1) i = 1
exact Finsupp.single_eq_same