[proofplan] We construct an integral basis by a minimality argument on the discriminant. Start with any $\mathbb{Q}$-basis of $L$ contained in $\mathcal{O}_L$ — easy to produce by clearing denominators. The discriminant of such a basis is a nonzero integer. Among all $\mathbb{Q}$-bases of $L$ contained in $\mathcal{O}_L$, pick one minimizing $|\Delta|$. Such a minimizer must be an integral basis: if some element of $\mathcal{O}_L$ had a non-integer coefficient in this basis, a change-of-basis argument would replace one basis vector with one of strictly smaller discriminant, contradicting minimality. Since the resulting integral basis has $n$ elements, $\mathcal{O}_L \cong \mathbb{Z}^n$ as a $\mathbb{Z}$-module. [/proofplan]

[step:Produce a $\mathbb{Q}$-basis of $L$ lying inside $\mathcal{O}_L$]Start with any $\mathbb{Q}$-basis $\beta_1, \ldots, \beta_n$ of $L$ (which exists because $[L:\mathbb{Q}] = n$ as $\mathbb{Q}$-vector spaces). Each $\beta_k$ is algebraic over $\mathbb{Q}$; let $p_{\beta_k}(t) = t^{m_k} + c_{k,m_k-1} t^{m_k-1} + \cdots + c_{k,0} \in \mathbb{Q}[t]$ be its minimal polynomial, and let $d_k \in \mathbb{Z}_{>0}$ be a common denominator of the coefficients $c_{k,0}, \ldots, c_{k,m_k-1}$. Then \begin{align*} q_k(t) := d_k^{m_k}\, p_{\beta_k}(t/d_k) = t^{m_k} + d_k c_{k,m_k-1} t^{m_k-1} + \cdots + d_k^{m_k} c_{k,0} \end{align*} is monic with integer coefficients, and $q_k(d_k \beta_k) = d_k^{m_k} p_{\beta_k}(\beta_k) = 0$. Hence $d_k \beta_k \in \mathcal{O}_L$ by definition. Set $\alpha_k := d_k \beta_k$. Then $\alpha_1, \ldots, \alpha_n \in \mathcal{O}_L$, and since the $d_k$ are nonzero scalars, $(\alpha_k)$ is still a $\mathbb{Q}$-basis of $L$.[/step]

[guided]The first task is to convince ourselves there exists a $\mathbb{Q}$-basis of $L$ all of whose members lie in $\mathcal{O}_L$ — this is the starting point for the minimality argument. **Existence of a $\mathbb{Q}$-basis in $L$.** By definition of "number field", $L/\mathbb{Q}$ is a finite extension of degree $n$, which means $L$ is an $n$-dimensional $\mathbb{Q}$-vector space. Any $n$-dimensional $\mathbb{Q}$-vector space has a basis, so pick any $\mathbb{Q}$-basis $\beta_1, \ldots, \beta_n$ of $L$. **Clearing denominators.** These $\beta_k$ are algebraic over $\mathbb{Q}$ (every element of a finite extension is algebraic) but need not be algebraic *integers*. The minimal polynomial $p_{\beta_k} \in \mathbb{Q}[t]$ is a monic polynomial with rational — but perhaps not integral — coefficients. To fix this, we rescale. Let $d_k \in \mathbb{Z}_{>0}$ be a common denominator for the coefficients of $p_{\beta_k}$. Consider \begin{align*} q_k(t) := d_k^{m_k}\, p_{\beta_k}(t/d_k), \end{align*} where $m_k = \deg p_{\beta_k}$. This is still monic (leading term: $d_k^{m_k} \cdot (t/d_k)^{m_k} = t^{m_k}$) and now has integer coefficients (the $k$-th coefficient $d_k^{m_k - (m_k - k)} c_{k,k} = d_k^k c_{k,k}$ — wait, let us compute carefully): \begin{align*} d_k^{m_k} (t/d_k)^j \cdot c_{k,j} = d_k^{m_k - j} c_{k,j} t^j. \end{align*} For $j = m_k$ the coefficient is $d_k^0 \cdot 1 = 1$ (monic), and for $j < m_k$ the coefficient is $d_k^{m_k - j} c_{k,j}$, which is a rational whose denominator divides $d_k^j$ (since $d_k c_{k,j} \in \mathbb{Z}$ by choice of $d_k$, hence $d_k^{m_k-j} c_{k,j} = d_k^{m_k-j-1} \cdot (d_k c_{k,j}) \in \mathbb{Z}$ for $m_k - j \geq 1$). So $q_k \in \mathbb{Z}[t]$. Substituting $t = d_k \beta_k$: \begin{align*} q_k(d_k \beta_k) = d_k^{m_k} p_{\beta_k}(\beta_k) = d_k^{m_k} \cdot 0 = 0, \end{align*} so $d_k \beta_k$ is a root of a monic polynomial in $\mathbb{Z}[t]$ — hence an algebraic integer. Since $d_k \beta_k \in L$ too, $d_k \beta_k \in \mathcal{O}_L$. Setting $\alpha_k := d_k \beta_k$: the $\alpha_k$ are elements of $\mathcal{O}_L$, and they are obtained from a basis $(\beta_k)$ by multiplying by nonzero scalars $d_k \in \mathbb{Q}^\times$, which preserves linear independence. Thus $\alpha_1, \ldots, \alpha_n$ is a $\mathbb{Q}$-basis of $L$ contained in $\mathcal{O}_L$.[/guided]

[step:Interpret the discriminant as a nonzero integer]For a $\mathbb{Q}$-basis $\gamma_1, \ldots, \gamma_n$ of $L$, define the **discriminant** \begin{align*} \Delta(\gamma_1, \ldots, \gamma_n) := \det\bigl(\operatorname{tr}_{L/\mathbb{Q}}(\gamma_i \gamma_j)\bigr)_{i,j=1}^n \in \mathbb{Q}. \end{align*} We assemble three facts. **(a) Discriminant of a basis in $\mathcal{O}_L$ lies in $\mathbb{Z}$.** If $\gamma_1, \ldots, \gamma_n \in \mathcal{O}_L$, each $\gamma_i \gamma_j \in \mathcal{O}_L$ (closed under multiplication by [Ring of Integers is a Ring](/theorems/1567)), so $\operatorname{tr}_{L/\mathbb{Q}}(\gamma_i \gamma_j) \in \mathbb{Z}$ (the trace of an algebraic integer is a rational integer, by [Integrality and the Characteristic Polynomial](/theorems/1574) applied to the characteristic polynomial). The determinant of an integer matrix is an integer, so $\Delta(\gamma_1, \ldots, \gamma_n) \in \mathbb{Z}$. **(b) Discriminant is nonzero.** By [Non-Degeneracy of the Trace Form](/theorems/1580) applied to $L/\mathbb{Q}$ (which is separable because $\mathbb{Q}$ is a perfect field of characteristic zero), the Gram matrix of the trace form has nonzero determinant. Hence $\Delta(\gamma_1, \ldots, \gamma_n) \neq 0$ for any $\mathbb{Q}$-basis of $L$. **(c) Change-of-basis formula.** If $\gamma_i' = \sum_k P_{ki} \gamma_k$ with $P \in \operatorname{GL}_n(\mathbb{Q})$, then \begin{align*} \Delta(\gamma_1', \ldots, \gamma_n') = (\det P)^2 \cdot \Delta(\gamma_1, \ldots, \gamma_n). \end{align*} Combining (a) and (b), for any $\mathbb{Q}$-basis of $L$ contained in $\mathcal{O}_L$, the discriminant is a nonzero integer. In particular $|\Delta(\alpha_1, \ldots, \alpha_n)| \in \mathbb{Z}_{>0}$, so the set \begin{align*} \mathcal{S} := \{|\Delta(\gamma_1, \ldots, \gamma_n)| : (\gamma_k) \text{ is a } \mathbb{Q}\text{-basis of } L \text{ with each } \gamma_k \in \mathcal{O}_L\} \subseteq \mathbb{Z}_{>0} \end{align*} is nonempty. By the well-ordering of $\mathbb{Z}_{>0}$, $\mathcal{S}$ has a minimum. Choose a $\mathbb{Q}$-basis $\gamma_1, \ldots, \gamma_n \in \mathcal{O}_L$ attaining this minimum and relabel it $\alpha_1, \ldots, \alpha_n$.[/step]

[guided]Now we introduce the gauge that drives the proof: the **discriminant** of a basis, which measures how "spread out" the basis is under the trace pairing. **Definition.** For a $\mathbb{Q}$-basis $\gamma_1, \ldots, \gamma_n$ of $L$, set \begin{align*} \Delta(\gamma_1, \ldots, \gamma_n) := \det\bigl(\operatorname{tr}_{L/\mathbb{Q}}(\gamma_i \gamma_j)\bigr)_{i,j=1}^n. \end{align*} This is the Gram determinant of the trace form $(x, y) \mapsto \operatorname{tr}_{L/\mathbb{Q}}(xy)$ in the basis $(\gamma_k)$. **Three properties of the discriminant.** *(a) Integrality when the basis lies in $\mathcal{O}_L$.* If each $\gamma_k \in \mathcal{O}_L$, then each $\gamma_i \gamma_j \in \mathcal{O}_L$ (by [Ring of Integers is a Ring](/theorems/1567), which tells us $\mathcal{O}_L$ is closed under multiplication). The trace of an element of $\mathcal{O}_L$ is in $\mathbb{Z}$: the characteristic polynomial of multiplication-by-$\gamma_i\gamma_j$ has integer coefficients (by [Integrality and the Characteristic Polynomial](/theorems/1574)), and the trace is (minus) its next-to-leading coefficient. Finally, the determinant of a matrix in $\mathbb{Z}^{n \times n}$ is an integer. So $\Delta \in \mathbb{Z}$. *(b) Non-vanishing.* By [Non-Degeneracy of the Trace Form](/theorems/1580), the Gram matrix of the trace form has nonzero determinant in *any* basis. The hypothesis of that theorem — separability of $L/\mathbb{Q}$ — is automatic because $\mathbb{Q}$ is a field of characteristic zero, hence perfect; all algebraic extensions of a perfect field are separable. So $\Delta(\gamma_1, \ldots, \gamma_n) \neq 0$ for every $\mathbb{Q}$-basis. *(c) Change-of-basis formula.* Suppose $\gamma_i' = \sum_k P_{ki} \gamma_k$ with $P = (P_{ki}) \in \operatorname{GL}_n(\mathbb{Q})$ the transition matrix. The Gram matrix transforms as $G' = P^\top G P$ (standard fact for bilinear forms), so $\det G' = (\det P)^2 \det G$, i.e., \begin{align*} \Delta(\gamma_1', \ldots, \gamma_n') = (\det P)^2 \Delta(\gamma_1, \ldots, \gamma_n). \end{align*} This is the squared-scaling we will exploit to produce a contradiction if the chosen basis is not an integral basis. **Applying well-ordering.** Consider the set \begin{align*} \mathcal{S} := \{|\Delta(\gamma_1, \ldots, \gamma_n)| : (\gamma_k) \text{ is a } \mathbb{Q}\text{-basis of } L \text{ with each } \gamma_k \in \mathcal{O}_L\}. \end{align*} By (a) and (b), $\mathcal{S} \subseteq \mathbb{Z}_{>0}$. By Step 1, $\mathcal{S} \neq \varnothing$. The well-ordering principle says every nonempty subset of $\mathbb{Z}_{>0}$ has a least element, so $\mathcal{S}$ has a minimum. Pick any $\mathbb{Q}$-basis $\alpha_1, \ldots, \alpha_n \in \mathcal{O}_L$ attaining the minimum of $\mathcal{S}$. We will prove that this minimizer is automatically an integral basis of $\mathcal{O}_L$.[/guided]

[step:Show that the minimizer is an integral basis via a substitution argument]We claim: every $x \in \mathcal{O}_L$ can be written $x = \sum_{k=1}^n n_k \alpha_k$ with $n_k \in \mathbb{Z}$. Let $x \in \mathcal{O}_L \subseteq L$. Since $\alpha_1, \ldots, \alpha_n$ is a $\mathbb{Q}$-basis of $L$, there exist unique $\lambda_1, \ldots, \lambda_n \in \mathbb{Q}$ with \begin{align*} x = \lambda_1 \alpha_1 + \lambda_2 \alpha_2 + \cdots + \lambda_n \alpha_n. \end{align*} Suppose for contradiction that some $\lambda_k \notin \mathbb{Z}$; WLOG (relabel the basis) take $k = 1$. Write \begin{align*} \lambda_1 = m_1 + \varepsilon_1, \qquad m_1 \in \mathbb{Z}, \; 0 < \varepsilon_1 < 1, \end{align*} using the floor $m_1 = \lfloor \lambda_1 \rfloor$ (so $\varepsilon_1 = \lambda_1 - m_1$ satisfies $0 \leq \varepsilon_1 < 1$; and $\varepsilon_1 > 0$ because otherwise $\lambda_1 = m_1 \in \mathbb{Z}$, contrary to assumption). Define \begin{align*} \alpha_1' := x - m_1 \alpha_1 = \varepsilon_1 \alpha_1 + \lambda_2 \alpha_2 + \cdots + \lambda_n \alpha_n. \end{align*} We verify two properties. **$\alpha_1' \in \mathcal{O}_L$:** indeed $x \in \mathcal{O}_L$ by hypothesis, $m_1 \alpha_1 \in \mathcal{O}_L$ (as $m_1 \in \mathbb{Z} \subseteq \mathcal{O}_L$ and $\alpha_1 \in \mathcal{O}_L$, using that $\mathcal{O}_L$ is a ring), so $\alpha_1' = x - m_1 \alpha_1 \in \mathcal{O}_L$ by closure under subtraction. **$(\alpha_1', \alpha_2, \ldots, \alpha_n)$ is a $\mathbb{Q}$-basis of $L$:** the transition matrix from $(\alpha_1, \alpha_2, \ldots, \alpha_n)$ to $(\alpha_1', \alpha_2, \ldots, \alpha_n)$ is \begin{align*} P = \begin{pmatrix} \varepsilon_1 & 0 & 0 & \cdots & 0 \\ \lambda_2 & 1 & 0 & \cdots & 0 \\ \lambda_3 & 0 & 1 & \cdots & 0 \\ \vdots & \vdots & \vdots & \ddots & \vdots \\ \lambda_n & 0 & 0 & \cdots & 1 \end{pmatrix}, \qquad \det P = \varepsilon_1 \neq 0, \end{align*} so $P \in \operatorname{GL}_n(\mathbb{Q})$. (Here columns $2, \ldots, n$ are standard basis vectors because we kept $\alpha_2, \ldots, \alpha_n$ unchanged, and the first column holds the coordinates of $\alpha_1'$ in the basis $(\alpha_k)$.) By the change-of-basis formula from Step 2 (c), \begin{align*} \Delta(\alpha_1', \alpha_2, \ldots, \alpha_n) = (\det P)^2 \cdot \Delta(\alpha_1, \ldots, \alpha_n) = \varepsilon_1^2 \cdot \Delta(\alpha_1, \ldots, \alpha_n). \end{align*} Taking absolute values and using $0 < \varepsilon_1 < 1$: \begin{align*} |\Delta(\alpha_1', \alpha_2, \ldots, \alpha_n)| = \varepsilon_1^2 \cdot |\Delta(\alpha_1, \ldots, \alpha_n)| < |\Delta(\alpha_1, \ldots, \alpha_n)|. \end{align*} But $(\alpha_1', \alpha_2, \ldots, \alpha_n)$ is a $\mathbb{Q}$-basis of $L$ contained in $\mathcal{O}_L$, so $|\Delta(\alpha_1', \alpha_2, \ldots, \alpha_n)| \in \mathcal{S}$, contradicting the minimality of $|\Delta(\alpha_1, \ldots, \alpha_n)|$. Therefore every $\lambda_k \in \mathbb{Z}$, and $x = \sum_k \lambda_k \alpha_k \in \sum_k \mathbb{Z} \alpha_k$.[/step]

[guided]We claim the minimizer $\alpha_1, \ldots, \alpha_n$ is an integral basis, meaning every element of $\mathcal{O}_L$ is a $\mathbb{Z}$-linear combination of the $\alpha_k$. Assume not, derive a contradiction with minimality. **Setup.** Take $x \in \mathcal{O}_L$ with rational coordinates $x = \sum \lambda_k \alpha_k$, $\lambda_k \in \mathbb{Q}$ (coordinates exist and are unique because $(\alpha_k)$ is a $\mathbb{Q}$-basis of $L$, and $\mathcal{O}_L \subseteq L$). Suppose some $\lambda_k \notin \mathbb{Z}$; WLOG $\lambda_1 \notin \mathbb{Z}$ (we can relabel the basis without affecting the discriminant up to sign, hence not affecting its absolute value). **The fractional part trick.** Write $\lambda_1 = m_1 + \varepsilon_1$ with $m_1 = \lfloor \lambda_1 \rfloor \in \mathbb{Z}$ and $\varepsilon_1 = \{\lambda_1\} \in [0, 1)$ the fractional part. Since $\lambda_1 \notin \mathbb{Z}$, $\varepsilon_1 \neq 0$, so $\varepsilon_1 \in (0, 1)$. The key is the key replacement: \begin{align*} \alpha_1' := x - m_1 \alpha_1. \end{align*} *Why this works.* Two things must hold simultaneously for $\alpha_1'$ to give us a contradiction: 1. **$\alpha_1'$ stays in $\mathcal{O}_L$.** Indeed $x \in \mathcal{O}_L$ and $\alpha_1 \in \mathcal{O}_L$, so their integer combination $x - m_1 \alpha_1 \in \mathcal{O}_L$. (We use that $\mathcal{O}_L$ is a ring, hence a $\mathbb{Z}$-module.) 2. **$(\alpha_1', \alpha_2, \ldots, \alpha_n)$ is still a $\mathbb{Q}$-basis.** Expanding $x$ in the $(\alpha_k)$-basis: \begin{align*} \alpha_1' = x - m_1 \alpha_1 = (\lambda_1 - m_1) \alpha_1 + \lambda_2 \alpha_2 + \cdots + \lambda_n \alpha_n = \varepsilon_1 \alpha_1 + \lambda_2 \alpha_2 + \cdots + \lambda_n \alpha_n. \end{align*} The transition matrix from $(\alpha_k)$ to $(\alpha_1', \alpha_2, \ldots, \alpha_n)$ is lower-triangular with diagonal $(\varepsilon_1, 1, 1, \ldots, 1)$, so its determinant is $\varepsilon_1$, which is nonzero. Hence the transition is in $\operatorname{GL}_n(\mathbb{Q})$. **The discriminant drops.** By the change-of-basis formula (c) from Step 2 with $\det P = \varepsilon_1$, \begin{align*} \Delta(\alpha_1', \alpha_2, \ldots, \alpha_n) = \varepsilon_1^2 \cdot \Delta(\alpha_1, \ldots, \alpha_n). \end{align*} Taking absolute values: $|\Delta(\alpha_1', \alpha_2, \ldots, \alpha_n)| = \varepsilon_1^2 \cdot |\Delta(\alpha_1, \ldots, \alpha_n)|$, and since $0 < \varepsilon_1 < 1$ we have $\varepsilon_1^2 < 1$, so the new discriminant absolute value is *strictly smaller* than the old. **Contradiction.** We have produced a $\mathbb{Q}$-basis of $L$ contained in $\mathcal{O}_L$ (namely $(\alpha_1', \alpha_2, \ldots, \alpha_n)$) with strictly smaller $|\Delta|$ than the supposed minimizer $(\alpha_1, \ldots, \alpha_n)$. This contradicts the fact that $|\Delta(\alpha_1, \ldots, \alpha_n)|$ is the minimum of $\mathcal{S}$. **Resolution.** The assumption "some $\lambda_k \notin \mathbb{Z}$" must be false. So for every $x \in \mathcal{O}_L$, every coordinate $\lambda_k \in \mathbb{Z}$, proving $x \in \sum_k \mathbb{Z} \alpha_k$.[/guided]

[step:Conclude existence of an integral basis and $\mathcal{O}_L \cong \mathbb{Z}^n$ as abelian groups]The previous step shows $\mathcal{O}_L \subseteq \sum_{k=1}^n \mathbb{Z} \alpha_k$. The reverse inclusion is trivial: each $\alpha_k \in \mathcal{O}_L$, so every $\mathbb{Z}$-linear combination $\sum n_k \alpha_k$ lies in the ring $\mathcal{O}_L$. Hence \begin{align*} \mathcal{O}_L = \sum_{k=1}^n \mathbb{Z} \alpha_k = \mathbb{Z} \alpha_1 + \cdots + \mathbb{Z} \alpha_n. \end{align*} Moreover the sum is direct as abelian groups: if $\sum n_k \alpha_k = 0$ with $n_k \in \mathbb{Z}$, then — viewing the $\alpha_k$ inside $L$ — the $\mathbb{Q}$-linear independence of $(\alpha_k)$ forces $n_k = 0$ for all $k$. Therefore the $\mathbb{Z}$-module map \begin{align*} \Phi: \mathbb{Z}^n &\to \mathcal{O}_L \\ (n_1, \ldots, n_n) &\mapsto \sum_{k=1}^n n_k \alpha_k \end{align*} is a $\mathbb{Z}$-module isomorphism: surjective by the containment $\mathcal{O}_L \subseteq \sum \mathbb{Z}\alpha_k$ (every element of $\mathcal{O}_L$ has integer coordinates), injective by the $\mathbb{Q}$-linear independence argument, and $\mathbb{Z}$-linear by construction. Since any $\mathbb{Z}$-module isomorphism is a fortiori an abelian group isomorphism, $\mathcal{O}_L \cong \mathbb{Z}^n$ as abelian groups. The sequence $(\alpha_1, \ldots, \alpha_n)$ is an **integral basis** of $\mathcal{O}_L$.[/step]

[guided]Steps 1–3 produced an $n$-tuple $\alpha_1, \ldots, \alpha_n \in \mathcal{O}_L$ with two properties: - They form a $\mathbb{Q}$-basis of $L$ (so $\mathbb{Q}$-linearly independent). - Every $x \in \mathcal{O}_L$ is a $\mathbb{Z}$-combination of them. We assemble these into the conclusion. **The $\mathbb{Z}$-module structure on $\mathcal{O}_L$.** The ring $\mathcal{O}_L$ is in particular an abelian group under addition. Since $\mathbb{Z} \subseteq \mathcal{O}_L$, it carries a natural $\mathbb{Z}$-module structure: $n \cdot x := nx$ (ring multiplication by $n \in \mathbb{Z}$). **Spanning.** By Step 3, every $x \in \mathcal{O}_L$ is of the form $x = \sum_k n_k \alpha_k$ with $n_k \in \mathbb{Z}$. So $\mathcal{O}_L \subseteq \sum_k \mathbb{Z} \alpha_k$. Conversely, each $\alpha_k \in \mathcal{O}_L$ and $\mathcal{O}_L$ is closed under $\mathbb{Z}$-linear combinations (it is a ring containing $\mathbb{Z}$). So $\sum_k \mathbb{Z} \alpha_k \subseteq \mathcal{O}_L$. Hence \begin{align*} \mathcal{O}_L = \mathbb{Z} \alpha_1 + \cdots + \mathbb{Z} \alpha_n. \end{align*} **$\mathbb{Z}$-linear independence.** We check the $\alpha_k$ are linearly independent over $\mathbb{Z}$. Suppose $\sum_k n_k \alpha_k = 0$ with $n_k \in \mathbb{Z}$. View this equation inside $L$. Since $\mathbb{Z} \subseteq \mathbb{Q}$, this is also a $\mathbb{Q}$-linear relation. But the $\alpha_k$ are $\mathbb{Q}$-linearly independent (they form a $\mathbb{Q}$-basis of $L$), so $n_k = 0$ for every $k$. $\mathbb{Z}$-linear independence holds. **Packaging as an isomorphism.** The map \begin{align*} \Phi: \mathbb{Z}^n &\to \mathcal{O}_L \\ (n_1, \ldots, n_n) &\mapsto \sum_{k=1}^n n_k \alpha_k \end{align*} is $\mathbb{Z}$-linear by construction (it extends the assignments $e_k \mapsto \alpha_k$ linearly). Surjectivity follows from $\mathcal{O}_L = \sum \mathbb{Z} \alpha_k$. Injectivity follows from $\mathbb{Z}$-linear independence: if $\Phi(n_1, \ldots, n_n) = 0$ then $\sum n_k \alpha_k = 0$, so all $n_k = 0$. Hence $\Phi$ is a $\mathbb{Z}$-module isomorphism, and so in particular an abelian group isomorphism. **Conclusion.** $\mathcal{O}_L \cong \mathbb{Z}^n$ as abelian groups (equivalently, as free $\mathbb{Z}$-modules of rank $n$). The $n$-tuple $(\alpha_1, \ldots, \alpha_n)$ constructed via the minimality argument is an **integral basis** of $\mathcal{O}_L$: a $\mathbb{Z}$-basis of $\mathcal{O}_L$ that is simultaneously a $\mathbb{Q}$-basis of $L$. **Remark on why the argument works.** The key tension we exploited is between two scales: $\mathcal{O}_L$ is a $\mathbb{Z}$-module but sits inside the $\mathbb{Q}$-vector space $L$. If a candidate basis had a non-integer coefficient, the fractional part produced a sub-module with *smaller* discriminant inside $\mathcal{O}_L$. The discriminant is the integral invariant that detects "size", and well-ordering of $\mathbb{Z}_{>0}$ guarantees the process terminates — it cannot decrease indefinitely within positive integers. Note that the argument does **not** give an effective algorithm for computing an integral basis: it only shows existence via well-ordering. Finding integral bases in practice usually proceeds via other techniques (e.g., Dedekind's criterion, Round 2 algorithm).[/guided]