Minkowski bound

To compute the class group we'd ideally check every ideal — but there are infinitely many. The saving grace is that we never have to look at large ideals: Minkowski's geometry of numbers guarantees that every ideal class already contains a representative whose norm is below a fixed, explicit threshold. So the infinite problem collapses to a finite search among small-norm ideals.

For a number field K of degree n with r_2 pairs of complex embeddings and discriminant d_K, the Minkowski bound is M_K = (n! / n^n) * (4/pi)^{r_2} * sqrt(|d_K|). The theorem asserts that every ideal class of O_K contains an integral ideal of norm at most M_K. The proof applies Minkowski's lattice-point theorem to the lattice O_K sitting in the Minkowski space R^{r_1} times C^{r_2}.

This is the practical engine for class group computations: list all prime ideals of norm up to M_K, find the relations among them coming from principal ideals, and the class group falls out. It also proves finiteness of the class number and, since M_K is at least 1 forces |d_K| greater than 1 for K not equal to Q, that every nontrivial number field has a ramified prime.