[proofplan] The strategy is to realize $\mathcal{O}_L/\mathfrak{a}$ as a quotient of a "nicer" ring whose finiteness is obvious. Concretely, any nonzero $\alpha \in \mathfrak{a}$ is a root of a monic polynomial over $\mathbb{Z}$, and the constant term of this polynomial is a nonzero integer that lies in the ideal $\mathfrak{a}$. Once we have a nonzero integer $a_0 \in \mathfrak{a} \cap \mathbb{Z}$, the principal ideal $\langle a_0 \rangle \subseteq \mathfrak{a}$ furnishes a surjection $\mathcal{O}_L/\langle a_0 \rangle \twoheadrightarrow \mathcal{O}_L/\mathfrak{a}$. The source is an abelian group isomorphic to $(\mathbb{Z}/a_0\mathbb{Z})^n$ via the integral basis, which is finite. Surjective images of finite sets are finite, so $\mathcal{O}_L/\mathfrak{a}$ is finite. [/proofplan]

[step:Produce a nonzero rational integer inside $\mathfrak{a}$ from a nonzero element $\alpha \in \mathfrak{a}$]Fix a nonzero element $\alpha \in \mathfrak{a}$ (which exists because $\mathfrak{a} \neq \{0\}$). By the [Integrality Criterion via Minimal Polynomial](/theorems/1570), the minimal polynomial $p_\alpha \in \mathbb{Q}[x]$ of $\alpha$ over $\mathbb{Q}$ has coefficients in $\mathbb{Z}$. Write \begin{align*} p_\alpha(x) &= x^m + a_{m-1}x^{m-1} + \cdots + a_1 x + a_0, \qquad a_0, \ldots, a_{m-1} \in \mathbb{Z}. \end{align*} The minimal polynomial of a nonzero element of a field is irreducible, hence $p_\alpha$ does not have $x$ as a factor, so $p_\alpha(0) \neq 0$; that is, $a_0 \neq 0$. Substituting $\alpha$ into $p_\alpha$ and isolating $a_0$: \begin{align*} 0 &= \alpha^m + a_{m-1}\alpha^{m-1} + \cdots + a_1 \alpha + a_0, \\ a_0 &= -\alpha\big(\alpha^{m-1} + a_{m-1}\alpha^{m-2} + \cdots + a_2 \alpha + a_1\big). \end{align*} We examine the right-hand side. The bracket lies in $\mathcal{O}_L$: by [Ring of Integers is a Ring](/theorems/1567) $\mathcal{O}_L$ is closed under the operations $+$ and $\cdot$, and $\alpha \in \mathcal{O}_L$, $a_i \in \mathbb{Z} \subseteq \mathcal{O}_L$. Therefore $\alpha \cdot (\cdot) \in \alpha \mathcal{O}_L \subseteq \mathfrak{a}$, the last inclusion holding because $\mathfrak{a}$ is an ideal containing $\alpha$. Hence $a_0 \in \mathfrak{a}$, and $a_0 \in \mathbb{Z}$ with $a_0 \neq 0$. This shows $\mathfrak{a} \cap \mathbb{Z}$ contains the nonzero integer $a_0$, so $\mathfrak{a} \cap \mathbb{Z} \neq \{0\}$.[/step]

[guided]We want to show two things for the given nonzero ideal $\mathfrak{a} \unlhd \mathcal{O}_L$: first, that $\mathfrak{a}$ contains a nonzero rational integer, and second, that $\mathcal{O}_L/\mathfrak{a}$ is finite. This step handles the first — and the integer we produce is precisely what will make the quotient finite in the next step. **Strategy.** An element $\alpha \in \mathcal{O}_L$ is, by definition, a root of a monic polynomial with $\mathbb{Z}$-coefficients. If that polynomial has a nonzero constant term $a_0$, then the relation $p_\alpha(\alpha) = 0$ can be rearranged to express $a_0$ as a multiple of $\alpha$; and multiples of $\alpha$ lie in $\mathfrak{a}$. The key subtlety is that we need $a_0 \neq 0$, which is why we use the *minimal* polynomial. **Picking $\alpha$.** Since $\mathfrak{a}$ is nonzero, choose any $\alpha \in \mathfrak{a} \setminus \{0\}$. **The minimal polynomial has integer coefficients.** By the [Integrality Criterion via Minimal Polynomial](/theorems/1570): $\alpha \in \mathcal{O}_L$ if and only if the minimal polynomial $p_\alpha \in \mathbb{Q}[x]$ of $\alpha$ over $\mathbb{Q}$ has all coefficients in $\mathbb{Z}$. Since $\alpha \in \mathfrak{a} \subseteq \mathcal{O}_L$, Theorem 1570 applies and \begin{align*} p_\alpha(x) &= x^m + a_{m-1}x^{m-1} + \cdots + a_1 x + a_0 \end{align*} with $a_0, \ldots, a_{m-1} \in \mathbb{Z}$. **Why $a_0 \neq 0$.** If $a_0$ were zero, we could factor $p_\alpha(x) = x \cdot q(x)$ with $q \in \mathbb{Q}[x]$ nonconstant and of positive degree. A minimal polynomial is irreducible over its base field (otherwise, one of its factors would annihilate $\alpha$ with smaller degree, contradicting minimality). But $p_\alpha = x \cdot q$ is reducible over $\mathbb{Q}$ when $\deg q \geq 1$. The only escape is $\deg p_\alpha = 1$, giving $p_\alpha = x$, which would mean $\alpha = 0$ — contrary to our choice. Hence $a_0 \neq 0$. **Extracting $a_0$ from the annihilation equation.** Evaluating $p_\alpha$ at $\alpha$: \begin{align*} \alpha^m + a_{m-1}\alpha^{m-1} + \cdots + a_1 \alpha + a_0 = 0. \end{align*} We solve for $a_0$, bringing all other terms to the other side, and factor an $\alpha$ out of each remaining term: \begin{align*} a_0 &= -\alpha^m - a_{m-1}\alpha^{m-1} - \cdots - a_1 \alpha \\ &= -\alpha \cdot \big(\alpha^{m-1} + a_{m-1}\alpha^{m-2} + \cdots + a_2 \alpha + a_1\big). \end{align*} **Why the bracketed factor lies in $\mathcal{O}_L$.** By [Ring of Integers is a Ring](/theorems/1567), $\mathcal{O}_L$ is a commutative ring containing $\mathbb{Z}$. Since $\alpha \in \mathcal{O}_L$ and $a_i \in \mathbb{Z} \subseteq \mathcal{O}_L$, the expression $\alpha^{m-1} + a_{m-1}\alpha^{m-2} + \cdots + a_1$ is a polynomial in $\alpha$ with $\mathcal{O}_L$-coefficients, hence lies in $\mathcal{O}_L$. **Why $a_0 \in \mathfrak{a}$.** The displayed equation says $a_0 = \alpha \cdot \beta$ for some $\beta \in \mathcal{O}_L$. Since $\mathfrak{a}$ is an ideal and $\alpha \in \mathfrak{a}$, we have $\alpha \cdot \beta \in \mathfrak{a}$, i.e., $a_0 \in \mathfrak{a}$. **Assembling the conclusion of this step.** $a_0 \in \mathfrak{a}$ and $a_0 \in \mathbb{Z}$ (coefficients of $p_\alpha$ are rational integers), hence $a_0 \in \mathfrak{a} \cap \mathbb{Z}$. And $a_0 \neq 0$ as shown. So $\mathfrak{a} \cap \mathbb{Z}$ is a nonzero ideal of $\mathbb{Z}$; in particular, $\mathfrak{a} \cap \mathbb{Z} \neq \{0\}$.[/guided]

[step:Use an integral basis to identify $\mathcal{O}_L/\langle a_0 \rangle$ with a finite product of cyclic groups]Let $a_0 \in \mathfrak{a} \cap \mathbb{Z}$ be the nonzero integer from the previous step. By [Existence of an Integral Basis](/theorems/1581), there exist $\omega_1, \ldots, \omega_n \in \mathcal{O}_L$ such that the map \begin{align*} \Phi: \mathbb{Z}^n &\to \mathcal{O}_L \\ (c_1, \ldots, c_n) &\mapsto c_1 \omega_1 + \cdots + c_n \omega_n \end{align*} is an isomorphism of abelian groups, where $n = [L : \mathbb{Q}]$. The principal ideal $\langle a_0 \rangle \unlhd \mathcal{O}_L$ equals $a_0 \mathcal{O}_L$. Under $\Phi$, this corresponds to $a_0 \mathbb{Z}^n \subseteq \mathbb{Z}^n$: explicitly, since $\Phi$ is $\mathbb{Z}$-linear and bijective, \begin{align*} \Phi^{-1}(a_0 \mathcal{O}_L) &= a_0 \Phi^{-1}(\mathcal{O}_L) = a_0 \mathbb{Z}^n. \end{align*} Therefore $\Phi$ descends to an isomorphism of abelian groups \begin{align*} \bar{\Phi}: \mathbb{Z}^n / a_0 \mathbb{Z}^n &\xrightarrow{\sim} \mathcal{O}_L / \langle a_0 \rangle. \end{align*} Finally, \begin{align*} \mathbb{Z}^n / a_0 \mathbb{Z}^n &\cong (\mathbb{Z}/a_0\mathbb{Z})^n \end{align*} as abelian groups, because the quotient acts coordinatewise. As $a_0 \neq 0$, the group $\mathbb{Z}/a_0\mathbb{Z}$ has cardinality $|a_0|$, so \begin{align*} |\mathcal{O}_L / \langle a_0 \rangle| &= |a_0|^n < \infty. \end{align*}[/step]

[guided]The previous step furnished a nonzero $a_0 \in \mathfrak{a} \cap \mathbb{Z}$. Our task now is to quantify "$\mathcal{O}_L/\langle a_0 \rangle$ is finite" — which will dominate the finiteness of $\mathcal{O}_L/\mathfrak{a}$ because $\langle a_0 \rangle \subseteq \mathfrak{a}$. **Integral basis.** By [Existence of an Integral Basis](/theorems/1581), $\mathcal{O}_L$ is a free abelian group of rank $n = [L : \mathbb{Q}]$: there is an integral basis $\omega_1, \ldots, \omega_n \in \mathcal{O}_L$ such that every $\alpha \in \mathcal{O}_L$ has a *unique* expression $\alpha = c_1 \omega_1 + \cdots + c_n \omega_n$ with $c_i \in \mathbb{Z}$. Concretely, this gives an isomorphism of abelian groups \begin{align*} \Phi: \mathbb{Z}^n &\to \mathcal{O}_L \\ (c_1, \ldots, c_n) &\mapsto \sum_{i=1}^n c_i \omega_i. \end{align*} **What is $\langle a_0 \rangle$?** The principal ideal generated by $a_0 \in \mathbb{Z} \subseteq \mathcal{O}_L$ is \begin{align*} \langle a_0 \rangle = a_0 \mathcal{O}_L = \{a_0 \cdot \beta : \beta \in \mathcal{O}_L\}. \end{align*} **Transporting $\langle a_0 \rangle$ through $\Phi$.** Since $\Phi$ is $\mathbb{Z}$-linear and a bijection, multiplication by the integer $a_0$ commutes with $\Phi$: \begin{align*} \Phi^{-1}(a_0 \mathcal{O}_L) &= a_0 \Phi^{-1}(\mathcal{O}_L) = a_0 \mathbb{Z}^n. \end{align*} (First equality uses $\Phi(a_0 \cdot c) = a_0 \Phi(c)$ for $c \in \mathbb{Z}^n$; second uses $\Phi^{-1}(\mathcal{O}_L) = \mathbb{Z}^n$ since $\Phi$ is a bijection.) **Passing to quotients.** A group isomorphism $\Phi: G \xrightarrow{\sim} H$ carrying a subgroup $G_0$ onto a subgroup $H_0$ descends to an isomorphism of quotients $G/G_0 \xrightarrow{\sim} H/H_0$. Applying this: \begin{align*} \bar{\Phi}: \mathbb{Z}^n/a_0\mathbb{Z}^n \xrightarrow{\sim} \mathcal{O}_L/\langle a_0 \rangle. \end{align*} **Computing $\mathbb{Z}^n/a_0\mathbb{Z}^n$.** The subgroup $a_0\mathbb{Z}^n = (a_0\mathbb{Z}) \times (a_0\mathbb{Z}) \times \cdots \times (a_0\mathbb{Z})$ is a product, so \begin{align*} \mathbb{Z}^n / a_0 \mathbb{Z}^n &= \mathbb{Z}^n / \prod_{i=1}^n a_0\mathbb{Z} \cong \prod_{i=1}^n \mathbb{Z}/a_0\mathbb{Z} = (\mathbb{Z}/a_0\mathbb{Z})^n. \end{align*} **Cardinality.** Since $a_0 \neq 0$, $|\mathbb{Z}/a_0\mathbb{Z}| = |a_0|$, so $|(\mathbb{Z}/a_0\mathbb{Z})^n| = |a_0|^n$. Combining with $\bar{\Phi}$: \begin{align*} |\mathcal{O}_L / \langle a_0 \rangle| &= |a_0|^n < \infty. \end{align*} So $\mathcal{O}_L/\langle a_0 \rangle$ is finite, with an explicit bound on its size.[/guided]

[step:Dominate $\mathcal{O}_L/\mathfrak{a}$ by $\mathcal{O}_L/\langle a_0 \rangle$ via a surjection]Since $a_0 \in \mathfrak{a}$ and $\mathfrak{a}$ is an ideal, $\langle a_0 \rangle = a_0 \mathcal{O}_L \subseteq \mathfrak{a}$. The inclusion of ideals $\langle a_0 \rangle \subseteq \mathfrak{a}$ induces, via the third isomorphism theorem, a surjective ring homomorphism \begin{align*} \pi: \mathcal{O}_L/\langle a_0 \rangle &\to \mathcal{O}_L/\mathfrak{a} \\ x + \langle a_0 \rangle &\mapsto x + \mathfrak{a}, \end{align*} well-defined because $\langle a_0 \rangle \subseteq \mathfrak{a}$ (so $x - x' \in \langle a_0 \rangle$ implies $x - x' \in \mathfrak{a}$). In particular $\pi$ is a surjection of sets, so \begin{align*} |\mathcal{O}_L/\mathfrak{a}| &\leq |\mathcal{O}_L/\langle a_0 \rangle| = |a_0|^n < \infty. \end{align*} Thus $\mathcal{O}_L/\mathfrak{a}$ is finite. Combined with the output of Step 1 — $\mathfrak{a} \cap \mathbb{Z} \neq \{0\}$ — both claims of the theorem are established.[/step]

[guided]We have shown (Step 2) that $\mathcal{O}_L/\langle a_0 \rangle$ is a finite set of size $|a_0|^n$. To deduce that $\mathcal{O}_L/\mathfrak{a}$ is finite, we compare the two quotients. **Why $\langle a_0 \rangle \subseteq \mathfrak{a}$.** The ideal $\mathfrak{a}$ contains $a_0$ (from Step 1). An ideal is closed under multiplication by elements of $\mathcal{O}_L$, so $\mathcal{O}_L \cdot a_0 \subseteq \mathfrak{a}$. The principal ideal $\langle a_0 \rangle$ is by definition $\mathcal{O}_L \cdot a_0$, hence $\langle a_0 \rangle \subseteq \mathfrak{a}$. **The quotient surjection.** Whenever $I \subseteq J$ are two ideals of a ring $R$, there is a surjective ring homomorphism $R/I \twoheadrightarrow R/J$ sending $x + I \mapsto x + J$. Well-definedness requires that $x + I = x' + I \implies x + J = x' + J$, i.e., $x - x' \in I \implies x - x' \in J$, which holds because $I \subseteq J$. Applying with $R = \mathcal{O}_L$, $I = \langle a_0 \rangle$, $J = \mathfrak{a}$: \begin{align*} \pi: \mathcal{O}_L/\langle a_0 \rangle &\twoheadrightarrow \mathcal{O}_L/\mathfrak{a}, \\ x + \langle a_0 \rangle &\mapsto x + \mathfrak{a}. \end{align*} **Why surjectivity forces finiteness.** If $X$ is a finite set and $\pi: X \to Y$ is a surjection, then $|Y| \leq |X| < \infty$, so $Y$ is finite. With $X = \mathcal{O}_L/\langle a_0 \rangle$ (of size $|a_0|^n$) and $Y = \mathcal{O}_L/\mathfrak{a}$: \begin{align*} |\mathcal{O}_L/\mathfrak{a}| &\leq |a_0|^n < \infty. \end{align*} **Assembling the theorem.** We have shown: 1. $\mathfrak{a} \cap \mathbb{Z}$ contains the nonzero integer $a_0$, so $\mathfrak{a} \cap \mathbb{Z} \neq \{0\}$. 2. $\mathcal{O}_L/\mathfrak{a}$ is a finite set (in fact, $|\mathcal{O}_L/\mathfrak{a}| \leq |a_0|^n$). Both conclusions of the theorem are established. **Remark on the bound.** The cardinality $|\mathcal{O}_L/\mathfrak{a}|$ — called the **ideal norm** $N(\mathfrak{a})$ — is an important invariant, though our bound $|a_0|^n$ is very coarse. The exact value depends on finer arithmetic properties of $\mathfrak{a}$, studied later in the theory.[/guided]