rw [degreeOf_eq_sup]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ degreeOf i p = 0 ↔ ∀ j ∈ p.support, j i = 0
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
⊢ (p.support.sup fun m => m i) = 0 ↔ ∀ j ∈ p.support, j i = 0