no goals
σ : Type u_2
τ : Type ?u.308829
R : Type u_1
S : Type ?u.308835
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
n : ℕ
r : R
⊢ ↑(homogeneousComponent n) (↑C r * φ) = ↑C r * ↑(homogeneousComponent n) φ
simp only [C_mul', LinearMap.map_smul]