no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.152343
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
⊢ i ∈ vars p ↔ ∃ d x, i ∈ d.support
classical simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff, exists_prop]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.152343
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
⊢ i ∈ vars p ↔ ∃ d x, i ∈ d.support
simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff, exists_prop]