completedRiemannZeta_residue_one

Mathlib.NumberTheory.LSeries.RiemannZeta

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

← MathLib Explorer

English

The residue of the Λ(s) at s = 1 equals 1.

Русский

У Λ(s) при s = 1 резидуал равен 1.

LaTeX

$$$\\mathrm{Res}_{s=1} \\Lambda(s) = 1$$$

Lean4

/-- The residue of `Λ(s)` at `s = 1` is equal to `1`. -/
theorem completedRiemannZeta_residue_one : Tendsto (fun s ↦ (s - 1) * completedRiemannZeta s) (𝓝[≠] 1) (𝓝 1) :=
  completedHurwitzZetaEven_residue_one 0

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

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

Разделы

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

Аффилиация

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