no goals
R : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
n : M
r : R
⊢ ↑(weightedHomogeneousComponent w n) (↑C r * φ) = ↑C r * ↑(weightedHomogeneousComponent w n) φ
simp only [C_mul', LinearMap.map_smul]