English
Let R be a commutative ring. The Chebyshev polynomial family satisfies an induction principle: if a predicate holds at 0 and 1, and if it holds for n+1 from n and n+2 from n, and similarly for negative indices, then it holds for all integers.
Русский
Пусть R — коммутативное кольцо. Семейство полиномов Чебышева удовлетворяет принципу индукции: если некоторое свойство верно для 0 и 1, и если из верности для n и n+1 следует верность для n+2, а также для отрицательных индексов, то свойство верно для всех целых чисел.
LaTeX
$$$ \forall (motive : \mathbb{Z} \to \text{Prop}),\ motive\ 0\to\ motive\ 1\to\left(\forall n:\mathbb{N},\ motive\ (n+1) \to\ motive\ n \to\ motive\ (n+2)\right)\to\left(\forall n:\mathbb{N},\ motive\ (-n) \to\ motive\ (-n+1) \to\ motive\ (-n-1)\right)\to\forall a:\mathbb{Z},\ motive\ a.$$
Lean4
theorem iterate_derivative_at_1_eq_zero_of_lt (n : ℕ) {ν k : ℕ} :
k < n - ν → (Polynomial.derivative^[k] (bernsteinPolynomial R n ν)).eval 1 = 0 :=
by
intro w
rw [flip' _ _ _ (tsub_pos_iff_lt.mp (pos_of_gt w)).le]
simp [Polynomial.eval_comp, iterate_derivative_at_0_eq_zero_of_lt R n w]
