no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ ↑derivative (eval₂ C q (↑C r)) = eval₂ C q (↑derivative (↑C r)) * ↑derivative q
rw [eval₂_C, derivative_C, eval₂_zero, 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 q p₁ p₂ : R[X]
ih₁ : ↑derivative (eval₂ C q p₁) = eval₂ C q (↑derivative p₁) * ↑derivative q
ih₂ : ↑derivative (eval₂ C q p₂) = eval₂ C q (↑derivative p₂) * ↑derivative q
⊢ ↑derivative (eval₂ C q (p₁ + p₂)) = eval₂ C q (↑derivative (p₁ + p₂)) * ↑derivative q
rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_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 q : R[X]
n : ℕ
r : R
ih : ↑derivative (eval₂ C q (↑C r * X ^ n)) = eval₂ C q (↑derivative (↑C r * X ^ n)) * ↑derivative q
⊢ ↑derivative (eval₂ C q (↑C r * X ^ (n + 1))) = eval₂ C q (↑derivative (↑C r * X ^ (n + 1))) * ↑derivative q
rw [pow_succ', ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X,
  derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]