funext — Mathlib

English

If two polynomials agree on every input from R, they are equal (extensionality for polynomials over an infinite domain).

Русский

Если два многочлена совпадают на каждом аргументе из R, то они равны (extensionality для многочленов над бесконечной областью).

LaTeX

$$[Infinite R] {p q : R[X]} (ext : ∀ r : R, p.eval r = q.eval r) : p = q$$

Lean4

theorem funext [Infinite R] {p q : R[X]} (ext : ∀ r : R, p.eval r = q.eval r) : p = q :=
  by
  rw [← sub_eq_zero]
  apply zero_of_eval_zero
  intro x
  rw [eval_sub, sub_eq_zero, ext]

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