MvPolynomial.funext

theorem MvPolynomial.funext : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : Infinite R] {σ : Type u_2} {p q : MvPolynomial σ R}, (∀ (x : σ → R), (MvPolynomial.eval x) p = (MvPolynomial.eval x) q) → p = q

The theorem `MvPolynomial.funext` asserts that for any two multivariate polynomials `p` and `q` over a commutative ring `R`, which is also an infinite integral domain, if these polynomials evaluate to the same value for any given assignment of the variables, then `p` and `q` are identical. The variables are indexed by the set `σ` and their values are elements of the ring `R`. In other words, two multivariate polynomials are equal if and only if they produce the same outputs for all possible inputs.

More concisely: For multivariate polynomials over a commutative infinite integral domain, equality of values under all variable assignments implies polynomial identity.