Finite-field theorem for finitely generated integer algebras (source code)

= Finite-field theorem for finitely generated integer algebras

A <field> that is a <finite-type integer algebra> has prime characteristic or zero. Prime characteristic and <Zariski lemma> make it a finite algebraic extension of a finite prime <field>. In characteristic zero, the same lemma makes it a number <field>; clearing finitely many coefficient denominators makes it integral over $\mathbb Z[1/N]$. The <integral field extension forces the base domain to be a field>, but a prime not dividing $N$ is not invertible there. This contradiction excludes characteristic zero.