Finite residue-field theorem for Gaussian integer orders (source code)

= Finite residue-field theorem for Gaussian integer orders

If $\alpha=a+bi$ is a <Gaussian integer> and $P$ is a nonzero <prime ideal> of $R=\mathbb Z[\alpha]$, then $R/P$ is a finite field. Complex conjugation preserves $R$, so a nonzero $\beta\in P$ gives the positive integer $\beta\bar\beta\in P$. Primality supplies a rational prime $p\in P$. Since $\alpha$ satisfies the monic polynomial $t^2-2at+a^2+b^2$, the ring $R/P$ is a quotient of $\mathbb F_p[t]/(\bar F)$ and has at most $p^2$ elements. It is a finite <integral domain>, hence a field. The proof does not require $R$ to be a <principal ideal domain>.