English
Two multivariate polynomials over an infinite domain are equal if they agree on the value at every assignment of the variables.
Русский
Два многочлена в нескольких переменных над бесконечным кольцом равны, если они дают одинаковые значения при любом заполнении переменных.
LaTeX
$$$(\forall x: \sigma \to R,\ eval_x p = \eval_x q) \Rightarrow p = q$$$
Lean4
/-- Two multivariate polynomials over an infinite integral domain are equal
if they are equal upon evaluating them on an arbitrary assignment of the variables. -/
theorem funext {σ : Type*} {p q : MvPolynomial σ R} (h : ∀ x : σ → R, eval x p = eval x q) : p = q :=
funext_set _ (fun _ ↦ Set.infinite_univ) fun _ _ ↦ h _
