neg

Mathlib.NumberTheory.LSeries.Linearity

URI: https://scilib.ai/kg/mathlib#LSeriesHasSum.neg

English

If f has L-series sum a at s, then −f has sum −a at s.

Русский

Если f имеет сумму L-series a в s, то −f имеет сумму −a в s.

LaTeX

$$$$ \mathrm{LSeriesHasSum}(-f)\; s\; (-a).$$$$

Lean4

theorem neg {f : ℕ → ℂ} {s a : ℂ} (hf : LSeriesHasSum f s a) : LSeriesHasSum (-f) s (-a) := by
  simpa [LSeriesHasSum, term_neg] using HasSum.neg hf

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

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

Разделы

Аффилиация

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