Density of polynomial nonvanishing

A nonzero multivariate polynomial over a domain with a perfect T1 topology is nonzero on a dense set of assignments. This includes infinitely many variables: every nonempty open set contains a box restricting only finitely many coordinates, with infinite sides. No continuity of the ring operations is needed for density.

Applied to the first nonzero homogeneous Taylor component, this lets one choose directions detecting ambient polynomial order inside any nonempty open set. Applied to p - C c, it shows that a polynomial whose evaluation is constant near a point is a constant polynomial. The algebraic input is Mathlib's MvPolynomial.funext_set.

theorem MvPolynomial.dense_setOf_eval_ne_zero {σ : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [TopologicalSpace R] [T1Space R] [PerfectSpace R] (p : MvPolynomial σ R) (hp : p ≠ 0) : Dense {x : σ → R | (eval x) p ≠ 0}

A nonzero polynomial is nonzero on a dense set, even with infinitely many variables. Only the perfect T1 topology on the coefficient domain is needed.

theorem MvPolynomial.eq_C_of_eventually_eval_eq {σ : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [TopologicalSpace R] [T1Space R] [PerfectSpace R] {p : MvPolynomial σ R} {a : σ → R} {c : R} (h : ∀ᶠ (x : σ → R) in nhds a, (eval x) p = c) : p = C c

A polynomial whose evaluation equals c on a neighbourhood of some assignment is the constant polynomial C c, even with infinitely many variables.