LSeriesSummable_zero

Mathlib.NumberTheory.LSeries.Basic

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

English

The L-series of the zero sequence is summable for every s.

Русский

L-серия нулевой последовательности суммируема для любого s.

LaTeX

$$LSeriesSummable(0,s) for all s$$

Lean4

@[simp]
theorem LSeriesSummable_zero {s : ℂ} : LSeriesSummable 0 s := by
  simp [LSeriesSummable, funext (term_def 0 s), summable_zero]

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

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

Разделы

Аффилиация

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