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 #
mv_polynomial.funext
: two polynomialsφ ψ : mv_polynomial σ R
over an infinite integral domainR
are equal ifeval x φ = eval x ψ
for allx : σ → R
.
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