expZeta_zero — Mathlib

English

The exponential-transform zeta function at 0 coincides with the Riemann zeta function: expZeta(0) = riemannZeta.

Русский

Функция expZeta в точке 0 совпадает с дзета Римана: expZeta(0) = riemannZeta.

LaTeX

$$$\\\\mathrm{expZeta}(0) = \\\\mathrm{riemannZeta}$$$

Lean4

theorem expZeta_zero : expZeta 0 = riemannZeta := by
  ext1 s
  rw [expZeta, cosZeta_zero, add_eq_left, mul_eq_zero, eq_false_intro I_ne_zero, false_or, ← eq_neg_self_iff, ←
    sinZeta_neg, neg_zero]

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