TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Finiteness of the number-field class group

Statement

Assume the Axiom of Choice (The Axiom of Choice). For every number field $K$ , the ideal class group $Cl (O_{K})$ (The ideal class group) is finite.

Facts & Assumptions

Given: The Axiom of Choice and a number field $K$ of degree $n$ and signature $(r_{1}, r_{2})$ , with Minkowski constant $M_{K} = (4 / π)^{r_{2}} (n! / n^{n}) \sqrt{∣ d_{K} ∣}$ .

[F1]

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

[F2]

For every real $B \geq 1$ there are only finitely many nonzero integral $O_{K}$ -ideals $b$ with $N b \leq B$ (Finitely many ideals of bounded norm).

[F3]

$Cl (O_{K})$ is the quotient of the group of nonzero fractional ideals by the subgroup of nonzero principal fractional ideals, and multiplication descends to a well-defined product on it; in particular there is a canonical class map $b \mapsto [b]$ from nonzero integral ideals to $Cl (O_{K})$ (The ideal class group, The ideal class group quotient is well defined).

Proof

1.1F2given

Put $B : = \max {M_{K}, 1} \geq 1$ ; by [F2] the set $S$ of nonzero integral ideals $b \subseteq O_{K}$ with $N b \leq B$ is finite.

2.1F2step 1.1

$S$ contains $O_{K}$ itself, of norm $1 \leq B$ , but only its finiteness is used below.

2.2F3step 1.1

By [F3] let $φ : S \to Cl (O_{K})$ be the class map $φ (b) = [b]$ .

3.1F1step 1.1step 2.2

The map $φ$ is surjective: for any class $[J] \in Cl (O_{K})$ , [F1] supplies an integral ideal $b$ with $[b] = [J]$ and $N b \leq M_{K} \leq B$ , so $b \in S$ and $φ (b) = [J]$ .

4.1step 1.1step 3.1∎

A set admitting a surjection from the finite set $S$ is finite, so $Cl (O_{K})$ is finite.

Remarks

The proof is a pure surjectivity argument: finiteness of the class group follows from the bound on representatives and the finiteness of ideals of bounded norm, with no further structure of the group used. The Choice assumption is inherited from the Minkowski bound route; the finiteness of ideals of bounded norm itself is choice-free. The set $S$ is explicit in terms of $O_{K}$ , the signature, and $∣ d_{K} ∣$ through $M_{K}$ .

Depends on

Used by

S-unit theorem Theorem

Dependency tree · two levels

21 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)