The zero set of a nonzero multivariate polynomial over a domain is null for any finite product of copies of an atomless finite measure.

import Definitions.Def_TypeDensity_Basic
import Definitions.Def_TypeDensity_Measure_AdicCylinders
import Mathlib.FieldTheory.RatFunc.Basic
import Mathlib.MeasureTheory.Measure.Haar.Unique
import Mathlib.NumberTheory.ArithmeticFunction.Moebius
import Mathlib.NumberTheory.Padics.PadicIntegers
import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
import Mathlib.RingTheory.MvPowerSeries.Basic
import Mathlib.RingTheory.RamificationInertia.Basic
import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
import Mathlib.Topology.Algebra.MvPolynomial
set_option autoImplicit false

open TypeDensity
open MeasureTheory
open scoped BigOperators ENNReal

theorem TypeDensity.mvPolynomial_zero_null {R : Type} [CommRing R] [IsDomain R]
    [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] [SecondCountableTopology R]
    [MeasurableSpace R] [BorelSpace R]
    (ν : Measure R) [IsFiniteMeasure ν] [NullSingletonClass ν] :
    ∀ (n : ℕ) (P : MvPolynomial (Fin n) R), P ≠ 0 →
      Measure.pi (fun _ : Fin n => ν) {x | MvPolynomial.eval x P = 0} = 0 := by sorry