no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.151305
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Nontrivial R
⊢ vars (X n) = {n}
rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single_ne_zero _ (one_ne_zero' ℕ)]