mathlib documentation

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 #

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.

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