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
⊢ ↑derivative (↑C a * X) = ↑C a
simp [C_mul_X_eq_monomial, derivative_monomial, Nat.cast_one, mul_one]