R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((↑derivative^[k]) (bernsteinPolynomial R n ν)) = 0
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
⊢ k < n - ν → eval 1 ((↑derivative^[k]) (bernsteinPolynomial R n ν)) = 0
intro w
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((↑derivative^[k]) (comp (bernsteinPolynomial R n (n - ν)) (1 - X))) = 0
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((↑derivative^[k]) (bernsteinPolynomial R n ν)) = 0
rw [flip' _ _ _ (tsub_pos_iff_lt.mp (pos_of_gt w)).le]
no goals
R : Type u_1
inst✝ : CommRing R
n ν k : ℕ
w : k < n - ν
⊢ eval 1 ((↑derivative^[k]) (comp (bernsteinPolynomial R n (n - ν)) (1 - X))) = 0
simp [Polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w]