English
Two multivariate polynomials over a domain are equal if their evaluations agree at every input vector x: eval_x p = eval_x q for all x.
Русский
Два многочлена в нескольких переменных над интегрируемым кольцом равны, если их значения совпадают на всём множестве аргументов: eval_x p = eval_x q для всех x.
LaTeX
$$$\forall x,\ eval_x(p) = eval_x(q) \Rightarrow p = q$$$
Lean4
/-- Two multivariate polynomials over an integral domain are equal
if they are equal when evaluated anywhere in a box with infinite sides. -/
theorem funext_set (h : ∀ x ∈ Set.pi .univ s, eval x p = eval x q) : p = q :=
by
suffices ∀ p, (∀ x ∈ Set.pi .univ s, eval x p = 0) → p = 0
by
rw [← sub_eq_zero, this (p - q)]
intro x hx
simp_rw [map_sub, h x hx, sub_self]
intro p h
obtain ⟨n, f, hf, p, rfl⟩ := exists_fin_rename p
suffices p = 0 by rw [this, map_zero]
refine funext_fin (s ∘ f) (fun _ ↦ hs _) fun x hx ↦ ?_
choose g hg using fun i ↦ (hs i).nonempty
convert h (Function.extend f x g) fun i _ ↦ ?_
· simp only [eval, eval₂Hom_rename, Function.extend_comp hf]
obtain ⟨i, rfl⟩ | nex := em (∃ x, f x = i)
· rw [hf.extend_apply]; exact hx _ ⟨⟩
· simp_rw [Function.extend, dif_neg nex, hg]
