apply (degreeOf_eq_zero_iff i (P.prod id)).1 _ j hjp
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
hp : ∀ p ∈ P, ∀ j ∈ p.support, j i = 0
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ j i = 0
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
P : Finset (MvPolynomial ι R)
hp : ∀ p ∈ P, ∀ j ∈ p.support, j i = 0
j : ι →₀ ℕ
hjp : j ∈ (P.prod id).support
⊢ degreeOf i (P.prod id) = 0