derivative_zero — Mathlib

English

The derivative of Bernstein(n)(0) equals -n times Bernstein(n-1, 0).

Русский

Производная Bernstein(n)(0) равна -n умножить Bernstein(n-1, 0).

LaTeX

$$$\mathrm{derivative}(\bernsteinPolynomial R n 0) = -n \cdot \bernsteinPolynomial R (n-1) 0$$$

Lean4

theorem derivative_zero (n : ℕ) :
    Polynomial.derivative (bernsteinPolynomial R n 0) = -n * bernsteinPolynomial R (n - 1) 0 := by
  simp [bernsteinPolynomial, Polynomial.derivative_pow]

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