add

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#IsPoly.add

English

If f and g are polynomial-valued, then f + g is polynomial-valued.

Русский

Если f и g — полиномиальные функции, то f+g — полиномиальная функция.

LaTeX

$$$\text{IsPoly}(f) \land \text{IsPoly}(g) \Rightarrow \text{IsPoly}(f+g)$$$

Lean4

theorem add {f g : (α → ℕ) → ℤ} (hf : IsPoly f) (hg : IsPoly g) : IsPoly (f + g) := by rw [← sub_neg_eq_add];
  exact hf.sub hg.neg

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

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

Разделы

Аффилиация

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