Proving the derivative of a polynomial evaluates to zero

Stream: new members

[oishi]

How should I prove this example? Specifically, I want to prove that the derivative evaluates to 0 when x=1. (I'm not sure if my formulation of this expression is correct.) I would like to complete this proof using a polynomial.

$$(-1)^n (n)(n-1)\cdots(n-m+1)(1-x)^{n-m} = 0, when \ x = 1$$

import Mathlib

example (h: m < n): Polynomial.eval 1 ((⇑Polynomial.derivative)^[m] ((Polynomial.C (1:ℝ) - Polynomial.X) ^ n))  = 0 := by sorry

[Ruben Van de Velde]

Are you perhaps missing an assumption on m and n?

[oishi]

oh, yes, m < n.

[Ruben Van de Velde]

My first step was found by rw?:

rw [@Polynomial.iterate_derivative_eq_factorial_smul_sum]

[oishi]

I find something like this.

theorem Polynomial.aeval_iterate_derivative_of_lt
{R : Type u_1} [CommSemiring R] {A : Type u_3} [CommRing A] [Algebra R A]
(p : Polynomial R) (q : ℕ) (r : A) {p' : Polynomial A}
(hp : Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p')
{k : ℕ} (hk : k < q) :
(Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = 0