Existence of an integral basis (source code)

= Existence of an integral basis

= Every number field has an integral basis
{synonym}

Every degree-$n$ <number field> has a <ring of integers> that is a <free abelian group> of rank $n$. To prove this without assuming finite generation, scale a rational <basis> to <algebraic integers> $\alpha_1,\ldots,\alpha_n$ and set $M=\sum_j\mathbb Z\alpha_j$. Their <trace pairing> has an invertible <integer> <matrix> $T$, since the <trace form of a number field> is nondegenerate. For $x\in\mathcal O_K$, all $\operatorname{Tr}(x\alpha_j)$ are <integers>. The <adjugate matrix> formula gives $M\subseteq\mathcal O_K\subseteq(\det T)^{-1}M$. The <submodule theorem for free modules over a principal ideal domain> makes the middle group free of rank $n$, and a group <basis> is an <integral basis>.