no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_2
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
α : Type u_1
s : Finset α
f : α → σ →₀ ℕ
a : R
⊢ ↑(monomial (∑ i in s, f i)) a = ↑C a * ∏ i in s, ↑(monomial (f i)) 1
rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]