mathlib3 documentation

data.mv_polynomial.funext

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 #

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} :