bernoulli_eq_sub_sum — Mathlib

English

Rearrangement of Faulhaber: (n+1) B_n = (n+1) X^n − ∑_{k=0}^{n-1} binom(n+1,k) B_k.

Русский

Перестановка формулы Фаульхера: (n+1) B_n = (n+1) X^n − ∑_{k=0}^{n-1} binom(n+1,k) B_k.

LaTeX

$$(n+1) bernoulli(n) = monomial n (n+1) − ∑_{k=0}^{n-1} binom(n+1,k) bernoulli(k)$$

Lean4

/-- Another version of `Polynomial.sum_bernoulli`. -/
theorem bernoulli_eq_sub_sum (n : ℕ) :
    (n.succ : ℚ) • bernoulli n = monomial n (n.succ : ℚ) - ∑ k ∈ Finset.range n, ((n + 1).choose k : ℚ) • bernoulli k :=
  by rw [Nat.cast_succ, ← sum_bernoulli n, sum_range_succ, add_sub_cancel_left, choose_succ_self_right, Nat.cast_succ]

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