exact mem_support_iff.mp hb₁
case h.right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p ≠ 0
b : ι →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)) = Multiset.card (Finsupp.toMultiset b)
⊢ coeff b p ≠ 0
no goals