no goals
σ : Type u_2
R : Type u_1
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module (MvPolynomial σ R) A
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ ↑D (↑C a * f) = a • ↑D f
rw [C_mul', D.map_smul]