term_sub

Mathlib.NumberTheory.LSeries.Linearity

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

English

The term operator is additive with subtraction: term(f − g) s = term f s − term g s.

Русский

Оператор term совместим с вычитанием: term(f − g) s = term f s − term g s.

LaTeX

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

Lean4

theorem term_sub (f g : ℕ → ℂ) (s : ℂ) : term (f - g) s = term f s - term g s := by
  simp_rw [sub_eq_add_neg, term_add, term_neg]

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

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

Разделы

Аффилиация

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