Theorems · Theorem · commutative algebra

MvPolynomial.funext_set

∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {σ : Type u_2} {p q : MvPolynomial σ R} (s : σ → Set R),
  (∀ (i : σ), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (MvPolynomial.eval x) p = (MvPolynomial.eval x) q) → p = q

Two multivariate polynomials over an integral domain are equal if they are equal when evaluated anywhere in a box with infinite sides.

Defined in

Mathlib.Algebra.MvPolynomial.Funext

Cited by

2 results in Mathlib

Foundations

Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain