Ideal counting: average of the coefficients of $\zeta_K$

Proved

ClassNumberFormula.ideal_count_asymptotic

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

class-number-formulanumber-theory

Let $K$ be a number field with $r_1$ real places, $r_2$ complex places, regulator $\mathrm{Reg}_K$ , class number $h_K$ , $w_K$ roots of unity and discriminant $D_K$ . Then the number of nonzero ideals of $\mathcal O_K$ of norm at most $N$ satisfies

\lim_{N\to\infty}\frac{\#\{\mathfrak a\subseteq\mathcal O_K : 1\le N(\mathfrak a)\le N\}}{N} = \frac{2^{r_1}(2\pi)^{r_2}\,\mathrm{Reg}_K\,h_K}{w_K\sqrt{|D_K|}} .

In the source this is the lattice-point step of the general proof: the count is reduced, through the real and complex embeddings and Dirichlet's unit theorem, to counting lattice points in a region, which is approximated by the volume of the region.

Formalization Note The condition $1 \le N(\mathfrak a)$ excludes the zero ideal, whose norm is $0$ in Mathlib.

Preamble

import Mathlib
open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real

Formal statement

namespace ClassNumberFormula

theorem ideal_count_asymptotic (K : Type*) [Field K] [NumberField K] :
    Tendsto (fun N : ℕ =>
        (Nat.card {I : Ideal (𝓞 K) // 1 ≤ Ideal.absNorm I ∧ Ideal.absNorm I ≤ N} : ℝ) / N)
      atTop (𝓝 ((2 : ℝ) ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K *
          classNumber K / (torsionOrder K * Real.sqrt |(discr K : ℝ)|))) := by sorry

end ClassNumberFormula

Source

Wikipedia, "Class number formula" (revision oldid=1366411311), https://en.wikipedia.org/w/index.php?title=Class_number_formula&oldid=1366411311, section "Proof", fourth paragraph (general case: reduction to a lattice point count)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Ideal counting: average of the coefficients of ζK\zeta_KζK​

Ideal counting: average of the coefficients of $\zeta_K$