no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.44438
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
i : σ
⊢ i ∈ degrees p ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support
classical
simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset, exists_prop]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.44438
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p✝ q p : MvPolynomial σ R
i : σ
⊢ i ∈ degrees p ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support
simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset, exists_prop]