term_neg

Mathlib.NumberTheory.LSeries.Linearity

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

English

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

Русский

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

LaTeX

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

Lean4

theorem term_neg (f : ℕ → ℂ) (s : ℂ) : term (-f) s = -term f s := by ext ⟨- | n⟩ <;> simp [neg_div]

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

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

Разделы

Аффилиация

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