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
n : ℕ
⊢ ↑derivative (↑C a * X ^ n) = ↑C (a * ↑n) * X ^ (n - 1)
rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]