riemannZeta_zero

Mathlib.NumberTheory.LSeries.RiemannZeta

URI: https://scilib.ai/kg/mathlib#riemannZeta_zero

← MathLib Explorer

English

The zeta function at zero is −1/2: riemannZeta(0) = −1/2.

Русский

Значение дзета Римана в точке 0 равно −1/2: ζ(0) = −1/2.

LaTeX

$$$\\\\riemannZeta(0) = -\\\\tfrac{1}{2}$$$

Lean4

/-- We have `ζ(0) = -1 / 2`. -/
theorem riemannZeta_zero : riemannZeta 0 = -1 / 2 := by
  simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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