Solution (source code)

= Solution

For a <number field> $K$ of <degree of a field extension> $n$, an <integral basis> is a <basis> $\omega_1,\ldots,\omega_n$ over $\mathbb Q$ such that
$$
\mathcal O_K=\mathbb Z\omega_1\oplus\cdots\oplus\mathbb Z\omega_n.
$$
Thus every <algebraic integer> in $K$ has a unique expression with <integer> coefficients in this <basis>. Merely requiring its entries to be <algebraic integers> would not suffice: for example, $1,2\sqrt2$ is a rational <basis> of $\mathbb Q(\sqrt2)$ but misses the <algebraic integer> $\sqrt2$ in its integer span.

Here is a proof of the <existence of an integral basis>. Start with any rational <basis> $v_1,\ldots,v_n$. Each $v_j$ has a nonzero <integer> multiple $\alpha_j$ that is an <algebraic integer>. Indeed, if
$$
v^m+c_{m-1}v^{m-1}+\cdots+c_0=0,\qquad c_i\in\mathbb Q,
$$
choose a positive <integer> $q$ clearing all the denominators. Then $qv$ satisfies the <monic polynomial>
$$
X^m+qc_{m-1}X^{m-1}+q^2c_{m-2}X^{m-2}+\cdots+q^mc_0\in\mathbb Z[X].
$$
The $\alpha_j$ are still a rational <basis>. Put $M=\sum_j\mathbb Z\alpha_j$ and form the <matrix>
$$
T=(\operatorname{Tr}_{K/\mathbb Q}(\alpha_i\alpha_j))_{i,j},\qquad D=\det T.
$$
Its entries are <integers>, because products and sums of <algebraic integers> are <algebraic integers> and a rational <algebraic integer> is an <integer>. The <nondegeneracy of the trace form of a number field> gives $D\ne0$: if $x\ne0$, then $\operatorname{Tr}(xx^{-1})=n\ne0$.

For $x=\sum_j x_j\alpha_j\in\mathcal O_K$, each $\operatorname{Tr}(x\alpha_i)$ is an <integer>, so
$$
T(x_1,\ldots,x_n)^T\in\mathbb Z^n.
$$
The <adjugate matrix> formula for $T^{-1}$ gives $Dx_j\in\mathbb Z$. Consequently
$$
M\subseteq\mathcal O_K\subseteq D^{-1}M.
$$
The <submodule theorem for free modules over a principal ideal domain> says that every subgroup of the finite-rank <free abelian group> $D^{-1}M$ is again a <free abelian group> of rank at most $n$. Since $\mathcal O_K$ contains $M$, its rank is exactly $n$. A <basis> of this <free abelian group> is the required <integral basis>.