LSeries_neg

Mathlib.NumberTheory.LSeries.Linearity

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

English

The L-series of the negation equals the negation of the L-series: LSeries(-f) s = -LSeries f s.

Русский

Л-серия от отрицания равна отрицанию Л-серии: LSeries(-f) s = -LSeries f s.

LaTeX

$$$$ \mathrm{LSeries}(-f)\; s = -\mathrm{LSeries}(f)\; s. $$$$

Lean4

@[simp]
theorem LSeries_neg (f : ℕ → ℂ) (s : ℂ) : LSeries (-f) s = -LSeries f s := by simp [LSeries, term_neg_apply, tsum_neg]

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

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

Разделы

Аффилиация

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