hurwitzZeta_zero

Mathlib.NumberTheory.LSeries.RiemannZeta

URI: https://scilib.ai/kg/mathlib#HurwitzZeta.hurwitzZeta_zero

English

Evaluating Hurwitz zeta at 0 recovers the Riemann zeta function: hurwitzZeta(0) = riemannZeta.

Русский

Значение гиперуровня Хурвизаты при 0 равно дзета Римана: hurwitzZeta(0) = riemannZeta.

LaTeX

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

Lean4

theorem hurwitzZeta_zero : hurwitzZeta 0 = riemannZeta :=
  by
  ext1 s
  simpa [hurwitzZeta, hurwitzZetaEven_zero] using hurwitzZetaOdd_neg 0 s

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru