no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.127739
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : r ≠ 0
⊢ vars (↑(monomial s) r) = s.support
classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.127739
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : r ≠ 0
⊢ vars (↑(monomial s) r) = s.support
rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]