# mathlibdocumentation

data.mv_polynomial.funext

## 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 #

• mv_polynomial.funext: two polynomials φ ψ : mv_polynomial σ R over an infinite integral domain R are equal if eval x φ = eval x ψ for all x : σ → R.
theorem mv_polynomial.funext {R : Type u_1} [infinite R] {σ : Type u_2} {p q : R} (h : ∀ (x : σ → R), p = 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 mv_polynomial.funext_iff {R : Type u_1} [infinite R] {σ : Type u_2} {p q : R} :
p = q ∀ (x : σ → R), p = q