eq_zero_of_not_LSeriesSummable

Mathlib.NumberTheory.LSeries.Basic

URI: https://scilib.ai/kg/mathlib#LSeries.eq_zero_of_not_LSeriesSummable

English

If the L-series is not summable at s, then its value is zero.

Русский

Если L-ряд в точке s не суммируем, то его значение равно нулю.

LaTeX

$$¬LSeriesSummable(f,s) → LSeries(f,s) = 0$$

Lean4

theorem eq_zero_of_not_LSeriesSummable (f : ℕ → ℂ) (s : ℂ) : ¬LSeriesSummable f s → LSeries f s = 0 :=
  tsum_eq_zero_of_not_summable

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

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

Разделы

Аффилиация

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