case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : ↑derivative (comp p✝ q) = ↑derivative q * comp (↑derivative p✝) q
a✝ : ↑derivative (comp q✝ q) = ↑derivative q * comp (↑derivative q✝) q
⊢ ↑derivative (comp (p✝ + q✝) q) = ↑derivative q * comp (↑derivative (p✝ + q✝)) q

case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ ↑derivative (comp (↑(monomial n✝) a✝) q) = ↑derivative q * comp (↑derivative (↑(monomial n✝) a✝)) q
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]
⊢ ↑derivative (comp p q) = ↑derivative q * comp (↑derivative p) q
induction p using Polynomial.induction_on'
no goals
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q p✝ q✝ : R[X]
a✝¹ : ↑derivative (comp p✝ q) = ↑derivative q * comp (↑derivative p✝) q
a✝ : ↑derivative (comp q✝ q) = ↑derivative q * comp (↑derivative q✝) q
⊢ ↑derivative (comp (p✝ + q✝) q) = ↑derivative q * comp (↑derivative (p✝ + q✝)) q
simp [*, mul_add]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ ↑C a✝ * (↑n✝ * q ^ (n✝ - 1) * ↑derivative q) = ↑derivative q * (↑C a✝ * ↑n✝ * q ^ (n✝ - 1))
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ ↑derivative (comp (↑(monomial n✝) a✝) q) = ↑derivative q * comp (↑derivative (↑(monomial n✝) a✝)) q
simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C,
  zero_mul, C_eq_nat_cast, zero_add, RingHom.map_mul]
no goals
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : CommSemiring R
q : R[X]
n✝ : ℕ
a✝ : R
⊢ ↑C a✝ * (↑n✝ * q ^ (n✝ - 1) * ↑derivative q) = ↑derivative q * (↑C a✝ * ↑n✝ * q ^ (n✝ - 1))
ring