Finite-tuple weak-field property of the generic integral domain (source code)

= Finite-tuple weak-field property of the generic integral domain
{title2=$\neg\bigwedge_i\operatorname{Unit}(x_i)\ \Rightarrow\ \bigvee_i(x_i=0)$}

In the generic domain, negation of simultaneous invertibility of finitely many elements implies that one is zero. At a ring stage, localize at their product $t$. All become units, so a tuple satisfying the negation makes the localized stage empty. The <empty-cover criterion for the domain-classifying site> then says $A[1/t]=0$, hence $t$ is nilpotent. Repeated zero-product covers force one factor to vanish locally. The two-variable property conversely forces the integral-domain axiom in any nontrivial internal ring.