CorollaryStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passaudited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Class group generated by small prime ideals

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $K$ be a number field of degree $n$ and signature $(r_{1}, r_{2})$ , and let $M_{K} = (4 / π)^{r_{2}} (n! / n^{n}) \sqrt{∣ d_{K} ∣}$ . Then $Cl (O_{K})$ is generated by the classes of the nonzero prime ideals $p \subseteq O_{K}$ with $N p \leq M_{K}$ .

Facts & Assumptions

Given: The Axiom of Choice, a number field $K$ , its ring of integers $O_{K}$ , and a class $[J] \in Cl (O_{K})$ .

[F1]

Under the Axiom of Choice $O_{K}$ is a Dedekind domain (Rings of integers are Dedekind domains).

[F2]

Minkowski bound: every class in $Cl (O_{K})$ contains an integral ideal $b$ with $N b \leq M_{K}$ (Minkowski bound for ideal classes, The ideal class group).

[F3]

Every nonzero fractional ideal of a Dedekind domain factors uniquely as a product of powers of nonzero prime ideals, with only finitely many nonzero exponents and with nonnegative exponents on integral ideals (Unique factorization of nonzero fractional ideals into prime powers).

[F4]

For nonzero integral ideals $a, b$ one has $N (a b) = N a N b$ (Ideal norm is multiplicative), and for a nonzero prime ideal $p$ there is a rational prime $p$ with $N p = p^{f} \geq 2$ (The norm of a prime ideal).

[F5]

Multiplication of classes is well defined on $Cl (O_{K})$ and is compatible with products of fractional ideals (The ideal class group, The ideal class group quotient is well defined).

Proof

1.1F2given

Let $[J] \in Cl (O_{K})$ . By [F2] there is an integral ideal $b$ with $[b] = [J]$ and $N b \leq M_{K}$ ; in particular $b$ is nonzero.

2.1F1F3step 1.1

By [F1] and [F3], the nonzero integral ideal $b$ has a unique factorisation $b = p_{1}^{e_{1}} \dots p_{r}^{e_{r}}$ with the $p_{i}$ nonzero prime ideals of $O_{K}$ and integers $e_{i} \geq 1$ .

3.1F4step 1.1step 2.1algebra

By [F4], $N b = \prod_{i = 1}^{r} (N p_{i})^{e_{i}}$ with each $N p_{i} \geq 2$ ; since every factor of the positive integer $N b$ is at most $N b$ , each $N p_{i} \leq N b \leq M_{K}$ .

3.2F5step 1.1step 2.1

By [F5] the class of the product is the product of the classes: $[J] = [b] = \prod_{i = 1}^{r} [p_{i}]^{e_{i}}$ in $Cl (O_{K})$ .

4.1step 3.1step 3.2∎

Steps 3.1 and 3.2 exhibit every class $[J]$ as a product of classes of nonzero prime ideals $p$ with $N p \leq M_{K}$ ; hence those classes generate $Cl (O_{K})$ .

Remarks

Finite generation alone does not imply finiteness of a group. In the preceding Finiteness of the number-field class group, [F2] supplies an integral ideal of norm at most $M_{K}$ representing every class. The finite set of these bounded-norm ideals therefore surjects onto $Cl (O_{K})$ , which proves finiteness.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Algebraic Number Theory v3.08 (standard reference, not scraped)
William A. Stein, Algebraic Number Theory: A Computational Approach (standard reference, not scraped)