LSeriesSummable_one_iff

Mathlib.NumberTheory.LSeries.Dirichlet

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

← MathLib Explorer

English

Dirichlet character modulo 1 is the constant-1 function.

Русский

Dirichlet-символ модуля 1 есть константа 1.

LaTeX

$$$(χ \cdot) = 1$ for χ : DirichletCharacter R 1.$$

Lean4

/-- The `LSeries` of the constant sequence `1` converges at `s` if and only if `re s > 1`. -/
theorem LSeriesSummable_one_iff {s : ℂ} : LSeriesSummable 1 s ↔ 1 < s.re :=
  modOne_eq_one (χ := χ₁) ▸ LSeriesSummable_iff one_ne_zero χ₁

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

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

Разделы

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

Аффилиация

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