hurwitzZetaEven_apply_zero

Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

English

The value of hurwitzZetaEven a at s = 0 is -1/2 if a = 0, and 0 otherwise.

Русский

Значение hurwitzZetaEven a в s = 0 равно -1/2, если a = 0, и 0 в противном случае.

LaTeX

$$$\\forall a:\\text{UnitAddCircle},\\ hurwitzZetaEven(a,0) = \\operatorname{ite}(a=0,-\\tfrac{1}{2},0).$$$

Lean4

theorem hurwitzZetaEven_apply_zero (a : UnitAddCircle) : hurwitzZetaEven a 0 = if a = 0 then -1 / 2 else 0 :=
  Function.update_self ..

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

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

Разделы

Аффилиация

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