iterate_derivative_at_1_ne_zero — Mathlib

English

Let R be a CharZero commutative ring. For all n, ν with ν ≤ n, the value (n−ν)-th derivative of the Bernstein polynomial B_{n,ν} at 1 is nonzero.

Русский

Пусть R — коммутативное кольцо с CharZero. Для всех n, ν с ν ≤ n значение (n−ν)-й производной Bernstein-полиномa B_{n,ν} в точке 1 отлично от нуля.

LaTeX

$$$ (Polynomial.derivative^{n-\nu} (bernsteinPolynomial R n ν)).eval 1 \neq 0 $$$

Lean4

theorem iterate_derivative_at_1_ne_zero [CharZero R] (n ν : ℕ) (h : ν ≤ n) :
    (Polynomial.derivative^[n - ν] (bernsteinPolynomial R n ν)).eval 1 ≠ 0 :=
  by
  rw [bernsteinPolynomial.iterate_derivative_at_1 _ _ _ h, Ne, neg_one_pow_mul_eq_zero_iff, ← Nat.cast_succ, ←
    ascPochhammer_eval_cast, ← Nat.cast_zero, Nat.cast_inj]
  exact (ascPochhammer_pos _ _ (Nat.succ_pos ν)).ne'

Похожие утверждения