Definition
For any integer polynomial $f$ and $n\in\mathbb N$ we define `deriv_n f n` to be the $n$-th derivative of polynomial $f$. $h^{[n]}$ means $h\circ h\circ h\cdots\circ h$ $n$-times.
def deriv_n (f : ℤ[X]) (n : ℕ) : ℤ[X] := polynomial.derivative ^[n] f
Lemma
the zeroth derivative of polynomial $f$ is $f$ itself.
lemma zeroth_deriv (f : ℤ[X]) : deriv_n f 0 = f :=
Proof
QED.
This is purely definition of
deriv_n f n We also used $f^{[n]}=\mathrm{id}$ and $\mathrm{id} x = x$.
rw deriv_n, simp only [id.def, function.iterate_zero],
f : ℤ[X]
⊢ deriv_n f 0 = f
no goals
Lemma
the derivative of $f^{(n)}$ is $f^{(n+1)}$
lemma deriv_succ (f : ℤ[X]) (n : ℕ) : (deriv_n f n).derivative = (deriv_n f (n+1)) :=
Proof
QED.
By definition and $h^{[n+1]}=h\circ h^{[n]}$
rw [deriv_n, deriv_n, function.iterate_succ'],
f : ℤ[X],
n : ℕ
⊢ (deriv_n f n).derivative = deriv_n f (n + 1)
no goals
Lemma
the $n$-th derivative of zero polynomial is $0$
lemma deriv_zero_p (n : ℕ) : deriv_n 0 n = 0 :=
Proof
QED.
We prove by induction. Base case and inductive case can all be done with
simp
induction n with n hn; simp only [deriv_n, id.def, function.iterate_zero], rw <-deriv_n, assumption,
n : ℕ
⊢ deriv_n 0 n = 0
no goals
Lemma
If the $n$-th coefficient of $f$ is $a_n$, then the $n$-th coefficient in $f^{(k)}$ is $\left(\prod_{i=0}^{k-1} (n+k-i)\right)a_{n+k}$
lemma deriv_n_coeff (f : ℤ[X]) (k : ℕ) : ∀ n : ℕ, (deriv_n f k).coeff n = (∏ i in finset.range k, (n+k-i)) * (f.coeff (n+k)) :=
Proof
QED.
So we use induction on $k$
induction k with k ih,
f : ℤ[X],
k : ℕ
⊢ ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k)
2 goals
case nat.zero
f : ℤ[X]
⊢ ∀ (n : ℕ), (deriv_n f 0).coeff n = (∏ (i : ℕ) in finset.range 0, (↑n + ↑0 - ↑i)) * f.coeff (n + 0)
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k)
⊢ ∀ (n : ℕ),
(deriv_n f k.succ).coeff n =
(∏ (i : ℕ) in finset.range k.succ, (↑n + ↑(k.succ) - ↑i)) * f.coeff (n + k.succ)
For the zeroth derivative, $f^{(0)}=f$. This case is true by
simp.
simp only [add_zero, nat.nat_zero_eq_zero, one_mul, finset.range_zero, finset.prod_empty], rw deriv_n, simp only [forall_const, id.def, eq_self_iff_true, function.iterate_zero],
2 goals
case nat.zero
f : ℤ[X]
⊢ ∀ (n : ℕ), (deriv_n f 0).coeff n = (∏ (i : ℕ) in finset.range 0, (↑n + ↑0 - ↑i)) * f.coeff (n + 0)
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k)
⊢ ∀ (n : ℕ),
(deriv_n f k.succ).coeff n =
(∏ (i : ℕ) in finset.range k.succ, (↑n + ↑(k.succ) - ↑i)) * f.coeff (n + k.succ)
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k)
⊢ ∀ (n : ℕ),
(deriv_n f k.succ).coeff n =
(∏ (i : ℕ) in finset.range k.succ, (↑n + ↑(k.succ) - ↑i)) * f.coeff (n + k.succ)
Let us assume our claim is true for $k$ and consider the $m$-th coefficient.
intro m,
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k)
⊢ ∀ (n : ℕ),
(deriv_n f k.succ).coeff n =
(∏ (i : ℕ) in finset.range k.succ, (↑n + ↑(k.succ) - ↑i)) * f.coeff (n + k.succ)
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (deriv_n f k.succ).coeff m =
(∏ (i : ℕ) in finset.range k.succ, (↑m + ↑(k.succ) - ↑i)) * f.coeff (m + k.succ)
We know that $f^{(k+1)}=\left(f^{(k)}\right)'$ and for any polynomial $g$, the $m$-th coefficient of $g'$ is $(m+1)\times (m+1)$-th coefficient of $g$. Then we can use induction hypothesis with $m+1$.
rw [deriv_n, function.iterate_succ'], simp only [function.comp_app, int.coe_nat_succ], rw <-deriv_n,
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (deriv_n f k.succ).coeff m =
(∏ (i : ℕ) in finset.range k.succ, (↑m + ↑(k.succ) - ↑i)) * f.coeff (m + k.succ)
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (deriv_n f k).derivative.coeff m =
(∏ (i : ℕ) in finset.range k.succ, (↑m + (↑k + 1) - ↑i)) * f.coeff (m + k.succ)
rw polynomial.coeff_derivative, rw ih (m+1),
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (deriv_n f k).derivative.coeff m =
(∏ (i : ℕ) in finset.range k.succ, (↑m + (↑k + 1) - ↑i)) * f.coeff (m + k.succ)
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (∏ (i : ℕ) in finset.range k, (↑(m + 1) + ↑k - ↑i)) * f.coeff (m + 1 + k) * (↑m + 1) =
(∏ (i : ℕ) in finset.range k.succ, (↑m + (↑k + 1) - ↑i)) * f.coeff (m + k.succ)
rw finset.prod_range_succ, simp only [int.coe_nat_succ, int.nat_cast_eq_coe_nat],
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (∏ (i : ℕ) in finset.range k, (↑(m + 1) + ↑k - ↑i)) * f.coeff (m + 1 + k) * (↑m + 1) =
(∏ (i : ℕ) in finset.range k.succ, (↑m + (↑k + 1) - ↑i)) * f.coeff (m + k.succ)
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (∏ (i : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑i)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
The rest of the proves are trivial to a pair of human eyes. But we need to give computers some hint to solve this triviality.
have triv : (∏ (x : ℕ) in finset.range k, ((m:ℤ) + 1 + ↑k - ↑x)) = ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x),
case nat.succ
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ (∏ (i : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑i)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
2 goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ ∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ (∏ (i : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑i)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
{
2 goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ ∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ (∏ (i : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑i)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ ∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
apply congr_arg, ext, simp only [sub_left_inj], ring,
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ
⊢ ∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
no goals
}, rw triv,
no goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
replace triv : (m + 1 : ℤ) = (m + (k+1) - k:ℤ),
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
2 goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ ↑m + 1 = ↑m + (↑k + 1) - ↑k
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
{
2 goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ ↑m + 1 = ↑m + (↑k + 1) - ↑k
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + 1) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ ↑m + 1 = ↑m + (↑k + 1) - ↑k
rw add_sub_assoc, simp only [add_sub_cancel'],
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv :
∏ (x : ℕ) in finset.range k, (↑m + 1 + ↑k - ↑x) =
∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)
⊢ ↑m + 1 = ↑m + (↑k + 1) - ↑k
no goals
}, rw triv,
no goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + (↑k + 1) - ↑k) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
replace triv : f.coeff (m + 1 + k) = f.coeff (m + k.succ),
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + (↑k + 1) - ↑k) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
2 goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ f.coeff (m + 1 + k) = f.coeff (m + k.succ)
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : f.coeff (m + 1 + k) = f.coeff (m + k.succ)
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + (↑k + 1) - ↑k) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
{
2 goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ f.coeff (m + 1 + k) = f.coeff (m + k.succ)
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : f.coeff (m + 1 + k) = f.coeff (m + k.succ)
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + (↑k + 1) - ↑k) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ f.coeff (m + 1 + k) = f.coeff (m + k.succ)
rw nat.succ_eq_add_one, ring,
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : ↑m + 1 = ↑m + (↑k + 1) - ↑k
⊢ f.coeff (m + 1 + k) = f.coeff (m + k.succ)
no goals
},
no goals
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : f.coeff (m + 1 + k) = f.coeff (m + k.succ)
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + (↑k + 1) - ↑k) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
rw triv, ring,
f : ℤ[X],
k : ℕ,
ih : ∀ (n : ℕ), (deriv_n f k).coeff n = (∏ (i : ℕ) in finset.range k, (↑n + ↑k - ↑i)) * f.coeff (n + k),
m : ℕ,
triv : f.coeff (m + 1 + k) = f.coeff (m + k.succ)
⊢ (∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + 1 + k) * (↑m + (↑k + 1) - ↑k) =
((↑m + (↑k + 1) - ↑k) * ∏ (x : ℕ) in finset.range k, (↑m + (↑k + 1) - ↑x)) * f.coeff (m + k.succ)
no goals
Lemma
Like first derivative, higher derivatives still respect addition
lemma deriv_n_add (p q :ℤ[X]) (n : ℕ) : (deriv_n (p+q) n) = (deriv_n p n) + (deriv_n q n) :=
Proof
QED.
Lemma
For any polynomial $f$ with degree $d$, the $d+1$-th derivative is zero.
theorem deriv_too_much (f : ℤ[X]): (deriv_n f (f.nat_degree + 1)) = 0 :=
Proof
QED.
We prove that all coefficient of $f^{(d+1)}$ is zero.
ext,
f : ℤ[X]
⊢ deriv_n f (f.nat_degree + 1) = 0
f : ℤ[X],
n : ℕ
⊢ (deriv_n f (f.nat_degree + 1)).coeff n = 0.coeff n
We use lemma
deriv_n_coeff and all coefficient of zero polynomial is $0$.
rw deriv_n_coeff, simp only [int.coe_nat_succ, polynomial.coeff_zero, mul_eq_zero], right,
f : ℤ[X],
n : ℕ
⊢ (deriv_n f (f.nat_degree + 1)).coeff n = 0.coeff n
f : ℤ[X],
n : ℕ
⊢ f.coeff (n + (f.nat_degree + 1)) = 0
Then the problem reduces to prove that $d+1$-th coeffcient of $f$ is zero. But $f$ has degree $d$. So we just need $d< d+1$. This is proved by
linarith.
apply polynomial.coeff_eq_zero_of_nat_degree_lt, linarith,
f : ℤ[X],
n : ℕ
⊢ f.coeff (n + (f.nat_degree + 1)) = 0
no goals
Lemma
if $i+1\le n$ then $n-(i+1)+1=n-i$
private lemma nat_sub_eq (n i : ℕ) (h : i + 1 ≤ n) : (n - (i + 1) + 1) = n - i :=
Proof
QED.
Lemma
We have the pascal triangle
\[{n\choose k+1}+{n\choose k} = {n+1\choose k+1}\]
private lemma pascal_triangle (n k : ℕ) : (n.choose (k+1)) + (n.choose k) = (n+1).choose (k+1) :=
Proof
This is actually how
mathlib defined binomial coefficient.
exact add_comm (nat.choose n (k + 1)) (nat.choose n k),
n k : ℕ
⊢ n.choose (k + 1) + n.choose k = (n + 1).choose (k + 1)
no goals
We prove by induction on $n$.
induction n with n IH,
p q : ℤ[X],
n : ℕ
⊢ deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
2 goals
case nat.zero
p q : ℤ[X]
⊢ deriv_n (p * q) 0 =
∑ (k : ℕ) in finset.range 1, ⇑polynomial.C ↑(0.choose k) * deriv_n p (0 - k) * deriv_n q k
case nat.succ
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ deriv_n (p * q) n.succ =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
For $n=0$, we are using
zeroth_deriv.
simp only [zeroth_deriv, nat.choose_self, int.cast_coe_nat, ring_hom.eq_int_cast, one_mul, nat.cast_one, finset.sum_singleton, finset.range_one],
2 goals
case nat.zero
p q : ℤ[X]
⊢ deriv_n (p * q) 0 =
∑ (k : ℕ) in finset.range 1, ⇑polynomial.C ↑(0.choose k) * deriv_n p (0 - k) * deriv_n q k
case nat.succ
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ deriv_n (p * q) n.succ =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
case nat.succ
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ deriv_n (p * q) n.succ =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
{
case nat.succ
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ deriv_n (p * q) n.succ =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
case nat.succ
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ deriv_n (p * q) n.succ =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
For inductive case We use $(pq)^{(n+1)}=d(pq)^{(n)} $, inductive hypothesis and that derivative is linear.
rw deriv_n, rw function.iterate_succ', dsimp, rw <-deriv_n,
case nat.succ
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ deriv_n (p * q) n.succ =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ (deriv_n (p * q) n).derivative =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
rw IH, simp only [polynomial.derivative_sum, polynomial.derivative_mul, zero_mul, polynomial.derivative_C, zero_add, polynomial.derivative_sum, polynomial.derivative_mul, zero_mul, polynomial.derivative_C, zero_add],
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ (deriv_n (p * q) n).derivative =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (b : ℕ) in
finset.range n.succ,
(⇑polynomial.C ↑(n.choose b) * (deriv_n p (n - b)).derivative * deriv_n q b +
⇑polynomial.C ↑(n.choose b) * deriv_n p (n - b) * (deriv_n q b).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
The rest of the proves is essentially openning and closing brackets and renaming summing indeces.
rw finset.sum_add_distrib,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (b : ℕ) in
finset.range n.succ,
(⇑polynomial.C ↑(n.choose b) * (deriv_n p (n - b)).derivative * deriv_n q b +
⇑polynomial.C ↑(n.choose b) * deriv_n p (n - b) * (deriv_n q b).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (x : ℕ) in
finset.range n.succ,
⇑polynomial.C ↑(n.choose x) * (deriv_n p (n - x)).derivative * deriv_n q x +
∑ (x : ℕ) in
finset.range n.succ,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
conv_lhs {rw finset.sum_range_succ', rw finset.sum_range_succ, simp only [zeroth_deriv, nat.choose_self, one_mul, nat.choose_zero_right, int.coe_nat_zero, nat.sub_self, polynomial.C_1, int.coe_nat_succ, nat.sub_zero, zero_add]},
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (x : ℕ) in
finset.range n.succ,
⇑polynomial.C ↑(n.choose x) * (deriv_n p (n - x)).derivative * deriv_n q x +
∑ (x : ℕ) in
finset.range n.succ,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
have eq :
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
∑ (i : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
polynomial.C (n.choose (i + 1):ℤ) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(deriv_n p n).derivative * q +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(p * (deriv_n q n).derivative +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
∑ (x : ℕ) in finset.range n, polynomial.C (n.choose x:ℤ) * deriv_n p (n - x) * (deriv_n q x).derivative) =
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (i : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
polynomial.C (n.choose (i + 1):ℤ) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1)) +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n, polynomial.C (n.choose x:ℤ) * deriv_n p (n - x) * (deriv_n q x).derivative) +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
((deriv_n p n).derivative * q + (p * (deriv_n q n).derivative)) := by ring,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
rw [eq, <-finset.sum_add_distrib],
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
replace eq :
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(polynomial.C (n.choose (x + 1):ℤ) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
polynomial.C (n.choose x:ℤ) * deriv_n p (n - x) * (deriv_n q x).derivative)) =
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(polynomial.C (n.choose (x + 1):ℤ) * (deriv_n p (n - x)) * deriv_n q (x + 1) +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
polynomial.C (n.choose x:ℤ) * deriv_n p (n - x) * (deriv_n q (x+1)))),
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
2 goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
{
2 goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
apply finset.sum_congr, exact rfl, intros i hi, simp only [deriv_succ, int.cast_coe_nat, ring_hom.eq_int_cast, add_left_inj], simp only [finset.mem_range] at hi,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative),
i : ℕ,
hi : i < n
⊢ ↑(n.choose (i + 1)) * deriv_n p (n - (i + 1) + 1) * deriv_n q (i + 1) =
↑(n.choose (i + 1)) * deriv_n p (n - i) * deriv_n q (i + 1)
replace hi : i + 1 ≤ n := hi,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative),
i : ℕ,
hi : i < n
⊢ ↑(n.choose (i + 1)) * deriv_n p (n - (i + 1) + 1) * deriv_n q (i + 1) =
↑(n.choose (i + 1)) * deriv_n p (n - i) * deriv_n q (i + 1)
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative),
i : ℕ,
hi : i + 1 ≤ n
⊢ ↑(n.choose (i + 1)) * deriv_n p (n - (i + 1) + 1) * deriv_n q (i + 1) =
↑(n.choose (i + 1)) * deriv_n p (n - i) * deriv_n q (i + 1)
rw nat_sub_eq _ _ hi,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
(deriv_n p n).derivative * q +
(p * (deriv_n q n).derivative +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (i : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose (i + 1)) * (deriv_n p (n - (i + 1))).derivative * deriv_n q (i + 1) +
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative),
i : ℕ,
hi : i + 1 ≤ n
⊢ ↑(n.choose (i + 1)) * deriv_n p (n - (i + 1) + 1) * deriv_n q (i + 1) =
↑(n.choose (i + 1)) * deriv_n p (n - i) * deriv_n q (i + 1)
no goals
}, rw eq,
no goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
replace eq :
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(polynomial.C (n.choose (x + 1):ℤ) * (deriv_n p (n - x)) * deriv_n q (x + 1) +
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
polynomial.C (n.choose x:ℤ) * deriv_n p (n - x) * (deriv_n q (x+1)))) =
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
((polynomial.C (n.choose (x + 1):ℤ) + polynomial.C (n.choose x:ℤ)) * (deriv_n p (n - x)) * deriv_n q (x + 1))),
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
2 goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
{
2 goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
apply congr_arg, rw function.funext_iff, intro i, ring,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * (deriv_n p (n - (x + 1))).derivative * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * (deriv_n q x).derivative) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1))
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
no goals
}, rw eq,
no goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
replace eq :
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
((polynomial.C (n.choose (x + 1):ℤ) + polynomial.C (n.choose x:ℤ)) * (deriv_n p (n - x)) * deriv_n q (x + 1))) =
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
((polynomial.C (n.choose (x + 1) + (n.choose x):ℤ)) * (deriv_n p (n - x)) * deriv_n q (x + 1))),
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
2 goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
{
2 goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
apply congr_arg, rw function.funext_iff, intro i, simp only [int.cast_add, ring_hom.eq_int_cast],
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) * deriv_n p (n - x) * deriv_n q (x + 1) +
⇑polynomial.C ↑(n.choose x) * deriv_n p (n - x) * deriv_n q (x + 1)) =
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
no goals
}, rw eq,
no goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
replace eq :
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
((polynomial.C (n.choose (x + 1) + (n.choose x):ℤ)) * (deriv_n p (n - x)) * deriv_n q (x + 1))) =
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
(∑ (x : ℕ) in finset.range n,
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
((polynomial.C ((n+1).choose (x + 1):ℤ)) * (deriv_n p (n - x)) * deriv_n q (x + 1))),
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1) +
((deriv_n p n).derivative * q + p * (deriv_n q n).derivative) =
∑ (k : ℕ) in
finset.range n.succ.succ,
⇑polynomial.C ↑(n.succ.choose k) * deriv_n p (n.succ - k) * deriv_n q k
2 goals
p q : ℤ[X],
n : ℕ,
IH :
deriv_n (p * q) n =
∑ (k : ℕ) in finset.range n.succ, ⇑polynomial.C ↑(n.choose k) * deriv_n p (n - k) * deriv_n q k,
eq :
∑ (x : ℕ) in
finset.range n,
(⇑polynomial.C ↑(n.choose (x + 1)) + ⇑polynomial.C ↑(n.choose x)) * deriv_n p (n - x) *
deriv_n q (x + 1) =
∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * deriv_n q (x + 1)
⊢ ∑ (x : ℕ) in
finset.range n,
⇑polynomial.C (↑(n.choose (x + 1)) + ↑(n.choose x)) * deriv_n p (n - x) * de