term_add_apply

Mathlib.NumberTheory.LSeries.Linearity

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

English

For any f,g and s,n, the term of the sum at n equals the sum of the terms at n:

Русский

Для любых f,g и s,n выполнено: term(f+g) s n = term f s n + term g s n.

LaTeX

$$$$ \operatorname{term}(f+g) s n = \operatorname{term} f s n + \operatorname{term} g s n. $$$$

Lean4

theorem term_add_apply (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) : term (f + g) s n = term f s n + term g s n := by simp [term_add]

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

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

Разделы

Аффилиация

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