no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ ↑derivative (p ^ Nat.zero) = ↑C ↑Nat.zero * p ^ (Nat.zero - 1) * ↑derivative p
rw [pow_zero, derivative_one, Nat.cast_zero, C_0, zero_mul, zero_mul]
no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝¹ : ℕ
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
⊢ ↑derivative (p ^ Nat.succ n) = ↑C ↑(Nat.succ n) * p ^ (Nat.succ n - 1) * ↑derivative p
rw [p.derivative_pow_succ n, n.succ_sub_one, n.cast_succ]