no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a✝ b : R
n : ℕ
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (↑derivative^[k]) (↑C a * p) = ↑C a * (↑derivative^[k]) p
simp_rw [← smul_eq_C_mul, iterate_derivative_smul]