neg

Mathlib.NumberTheory.Dioph

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

English

If two polynomials agree at every input, then they are equal.

Русский

Если две полиномы совпадают на каждом входе, то они равны.

LaTeX

$$$\forall f,g:\ Poly(\alpha), (\forall x, f(x) = g(x)) \Rightarrow f = g$$$

Lean4

theorem neg {f : (α → ℕ) → ℤ} : IsPoly f → IsPoly (-f) := by rw [← zero_sub]; exact (IsPoly.const 0).sub

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

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

Разделы

Аффилиация

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