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
f x : σ → R
p : MvPolynomial σ R
s : R
⊢ ↑(eval x) (s • p) = s * ↑(eval x) p
rw [smul_eq_C_mul, (eval x).map_mul, eval_C]