derivative_bernoulli — Mathlib

English

For every k, the derivative of B_k equals k B_{k-1} (with B_{-1} interpreted appropriately at the base case).

Русский

Для каждого k производная B_k равна k B_{k-1} (с базовым случаем корректно определенным).

LaTeX

$$Polynomial.derivative(bernoulli(k)) = k * bernoulli(k-1)$$

Lean4

theorem derivative_bernoulli (k : ℕ) : Polynomial.derivative (bernoulli k) = k * bernoulli (k - 1) := by
  cases k with
  | zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
  | succ k => exact mod_cast derivative_bernoulli_add_one k

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