bernoulli_eval_zero — Mathlib

English

The evaluation of Bernoulli polynomials at 0 recovers the Bernoulli numbers: B_n(0) = B_n.

Русский

Значение Бернулли-полиномов в 0 восстанавливает числа Бернулли: B_n(0) = B_n.

LaTeX

$$$\bigl(Bernoulli(n)\bigr).eval(0) = bernoulli(n)$$$

Lean4

@[simp]
theorem bernoulli_eval_zero (n : ℕ) : (bernoulli n).eval 0 = _root_.bernoulli n :=
  by
  rw [bernoulli, eval_finset_sum, sum_range_succ]
  have : ∑ x ∈ range n, _root_.bernoulli x * n.choose x * 0 ^ (n - x) = 0 :=
    by
    apply sum_eq_zero fun x hx => _
    intro x hx
    simp [tsub_eq_zero_iff_le, mem_range.1 hx]
  simp [this]

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