no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
⊢ ↑(monomial s) a = ↑C a * Finsupp.prod s fun n e => X n ^ e
simp only [X_pow_eq_monomial, ← monomial_finsupp_sum_index, Finsupp.sum_single]