iterate_derivative_succ_at_0_eq_zero

English

For all commutative rings R, for all n, ν ∈ ℕ, the ν-th derivative of the Bernstein polynomial B_n,ν, evaluated at 0, is zero.

Русский

Для любого кольца R коммутативного типа для всех n, ν ∈ ℕ η-ой производной Bernstein полинома B_n,ν в точке 0 равна нулю.

LaTeX

$$$\\bigl( \\mathrm{derivative}^{\,\\nu}(\\mathrm{bernsteinPolynomial}\\;R\\;n\\; (\\nu+1)) \\bigr) \\!\\mathrm{.eval}\\ 0 = 0$$$

Lean4

@[simp]
theorem iterate_derivative_succ_at_0_eq_zero (n ν : ℕ) :
    (Polynomial.derivative^[ν] (bernsteinPolynomial R n (ν + 1))).eval 0 = 0 :=
  iterate_derivative_at_0_eq_zero_of_lt R n (lt_add_one ν)

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