Function extensionality for multivariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem mv_polynomial.funext {R : Type u_1} [comm_ring R] [is_domain R] [infinite R] {σ : Type u_2} {p q : mv_polynomial σ R} (h : ∀ (x : σ → R), ⇑(mv_polynomial.eval x) p = ⇑(mv_polynomial.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.

source

theorem mv_polynomial.funext_iff {R : Type u_1} [comm_ring R] [is_domain R] [infinite R] {σ : Type u_2} {p q : mv_polynomial σ R} :

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