## Function extensionality for multivariate polynomials #

In this file we show that two multivariate polynomials over an infinite integral domain are equal if they are equal upon evaluating them on an arbitrary assignment of the variables.

# Main declaration #

`MvPolynomial.funext`

: two polynomials`φ ψ : MvPolynomial σ R`

over an infinite integral domain`R`

are equal if`eval x φ = eval x ψ`

for all`x : σ → R`

.

theorem
MvPolynomial.funext
{R : Type u_1}
[CommRing R]
[IsDomain R]
[Infinite R]
{σ : Type u_2}
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
(h : ∀ (x : σ → R), (MvPolynomial.eval x) p = (MvPolynomial.eval x) q)
:

p = q

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
MvPolynomial.funext_iff
{R : Type u_1}
[CommRing R]
[IsDomain R]
[Infinite R]
{σ : Type u_2}
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
:

p = q ↔ ∀ (x : σ → R), (MvPolynomial.eval x) p = (MvPolynomial.eval x) q