term_neg_apply

Mathlib.NumberTheory.LSeries.Linearity

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

English

Applying negation to f yields the negation of the term of f: term(-f) s n = -term f s n.

Русский

Применение отрицания к f даёт −term f s n: term(-f) s n = − term f s n.

LaTeX

$$$$ \operatorname{term}(-f)\; s\; n = -\operatorname{term} f\; s\; n. $$$$

Lean4

theorem term_neg_apply (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : term (-f) s n = -term f s n := by simp [term_neg]

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

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

Разделы

Аффилиация

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