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_set {R : Type u_1} [CommRing R] [IsDomain R] {σ : Type u_2} {p q : MvPolynomial σ R} (s : σ → Set R) (hs : ∀ (i : σ), (s i).Infinite) (h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q) : p = q

Two multivariate polynomials over an integral domain are equal if they are equal when evaluated anywhere in a box with infinite sides.

theorem MvPolynomial.funext_set_iff {R : Type u_1} [CommRing R] [IsDomain R] {σ : Type u_2} {p q : MvPolynomial σ R} (s : σ → Set R) (hs : ∀ (i : σ), (s i).Infinite) : p = q ↔ ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q

theorem MvPolynomial.funext {R : Type u_1} [CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {p q : MvPolynomial σ R} (h : ∀ (x : σ → R), (eval x) p = (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 q : MvPolynomial σ R} : p = q ↔ ∀ (x : σ → R), (eval x) p = (eval x) q