no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
c : R
m : ℕ
⊢ ↑derivative ((X + ↑C c) ^ m) = ↑C ↑m * (X + ↑C c) ^ (m - 1)
rw [derivative_pow, derivative_X_add_C, mul_one]