ext

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#Poly.ext

English

Two polynomials are equal if they agree on all inputs.

Русский

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

LaTeX

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

Lean4

/-- Extensionality for `Poly α` -/
@[ext]
theorem ext {f g : Poly α} : (∀ x, f x = g x) → f = g :=
  DFunLike.ext _ _

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

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

Разделы

Аффилиация

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