Documentation

Mathlib.Data.MvPolynomial.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 #

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