riemannZeta_def_of_ne_zero — Mathlib

English

For any s ≠ 0, the Riemann zeta function satisfies ζ(s) = ζ̂(s) / Γ(s).

Русский

Для любого s ≠ 0 дзета Римана удовлетворяет ζ(s) = \hat{ζ}(s) / Γ(s).

LaTeX

$$$\\\\riemannZeta(s) = \\\\hat{\\\\zeta}(s) / \\\\Gamma(s) \\\\\\text{ for } s \\neq 0$$$

Lean4

theorem riemannZeta_def_of_ne_zero {s : ℂ} (hs : s ≠ 0) : riemannZeta s = completedRiemannZeta s / Gammaℝ s := by
  rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]

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