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
s : σ
a : R
n : ℕ
⊢ ↑C a * X s ^ n = ↑(monomial (Finsupp.single s n)) a
rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]