Prove2Me

K=Q(i)K=\mathbb Q(i): the residue of ζK\zeta_K at s=1s=1 is π/4\pi/4

Proved
ClassNumberFormula.gaussian_residue_eq_pi_div_four

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

class-number-formulanumber-theory

Let KK be a quadratic number field containing a square root of −1-1, so that K≅Q(i)K\cong\mathbb Q(i). Then

lim⁡s→1+(s−1) ζK(s)=π4.\lim_{s\to1^+}(s-1)\,\zeta_K(s) = \frac{\pi}{4}.

This is the case of the class number formula worked out in the source's proof: here r1=0r_1 = 0, r2=1r_2 = 1, hK=1h_K = 1, RegK=1\mathrm{Reg}_K = 1, wK=4w_K = 4 and DK=−4D_K = -4.

Formalization Note The limit is taken along real s→1+s\to1^+, using Mathlib's dedekindZeta (the Dirichlet series).

Preamble
import Mathlib
open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real
Formal statement
namespace ClassNumberFormula

theorem gaussian_residue_eq_pi_div_four (K : Type*) [Field K] [NumberField K]
    (hK : Module.finrank ℚ K = 2) (hi : ∃ i : K, i ^ 2 = -1) :
    Tendsto (fun s : ℝ => ((s : ℂ) - 1) * dedekindZeta K s) (𝓝[>] 1)
      (𝓝 ((π / 4 : ℝ) : ℂ)) := 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", second paragraph ("concluding that the residue is one quarter of pi")
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