Quadratic fields: $\zeta_K(s)=\zeta(s)L(s,\chi)$ , and the residue is $L(1,\chi)$

Open

ClassNumberFormula.quadratic_dedekindZeta_eq_zeta_mul_L

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

class-number-formulanumber-theory

Let $K$ be a quadratic number field with discriminant $d = D_K$ , and let $\chi$ be the Dirichlet character modulo $|d|$ given by the Kronecker symbol, $\chi(n) = \left(\frac{d}{n}\right)$ . Then:

for every $s$ with $\operatorname{Re}(s) > 1$ ,

\zeta_K(s) = \zeta(s)\,L(s,\chi);

the residue of $\zeta_K$ at $s = 1$ is $L(1,\chi)$ :

\lim_{s\to1^+}(s-1)\,\zeta_K(s) = L(1,\chi).

Together with the general residue formula, this is how Dirichlet's class number formula appears as a special case of the class number formula.

Formalization Note $\zeta$ is Mathlib's riemannZeta and $L(s,\chi)$ is DirichletCharacter.LFunction, the analytic continuation; for the nontrivial character $\chi$ its value at $s=1$ is the value of the continuation. The instance argument [NeZero |d|] only records $d \neq 0$ , which always holds.

Preamble

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

Formal statement

namespace ClassNumberFormula

theorem quadratic_dedekindZeta_eq_zeta_mul_L (K : Type*) [Field K] [NumberField K]
    (hK : Module.finrank ℚ K = 2) [NeZero (discr K).natAbs]
    (χ : DirichletCharacter ℂ (discr K).natAbs)
    (hχ : ∀ n : ℕ, χ n = (kroneckerSymbol (discr K) n : ℂ)) :
    (∀ s : ℂ, 1 < s.re → dedekindZeta K s = riemannZeta s * χ.LFunction s) ∧
    Tendsto (fun s : ℝ => ((s : ℂ) - 1) * dedekindZeta K s) (𝓝[>] 1)
      (𝓝 (χ.LFunction 1)) := 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 "Dirichlet class number formula" ("for a quadratic field K, the Dedekind zeta function is just

\zeta_K(s)=\zeta(s)L(s,\chi)

, and the residue is

L(1,\chi)

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

Quadratic fields: ζK(s)=ζ(s)L(s,χ)\zeta_K(s)=\zeta(s)L(s,\chi)ζK​(s)=ζ(s)L(s,χ), and the residue is L(1,χ)L(1,\chi)L(1,χ)

Quadratic fields: $\zeta_K(s)=\zeta(s)L(s,\chi)$ , and the residue is $L(1,\chi)$