riemannZeta_neg_nat_eq_bernoulli — Mathlib

English

For any k ∈ ℕ, riemannZeta(−k) = (−1)^k bernoulli(k+1)/(k+1).

Русский

Для любого k ∈ ℕ, riemannZeta(−k) = (−1)^k bernoulli(k+1)/(k+1).

LaTeX

$$$$ \operatorname{riemannZeta}(-k) = (-1)^k \frac{\mathbf{bernoulli}(k+1)}{k+1}. $$$$

Lean4

/-- Value of Riemann zeta at `-ℕ` in terms of `bernoulli`. -/
theorem riemannZeta_neg_nat_eq_bernoulli (k : ℕ) : riemannZeta (-k) = (-1 : ℂ) ^ k * bernoulli (k + 1) / (k + 1) := by
  rw [riemannZeta_neg_nat_eq_bernoulli', bernoulli, Rat.cast_mul, Rat.cast_pow, Rat.cast_neg, Rat.cast_one, ←
    neg_one_mul, ← mul_assoc, pow_succ, ← mul_assoc, ← mul_pow, neg_one_mul (-1), neg_neg, one_pow, one_mul]

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