For a fundamental discriminant $d$ , $\chi = \left(\frac{d}{\cdot}\right)$ is a Dirichlet character mod $|d|$

Proved

ClassNumberFormula.kronecker_is_dirichlet_character

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

class-number-formulanumber-theory

Let $d$ be a fundamental discriminant. Then there is a Dirichlet character $\chi$ modulo $|d|$ such that

\chi(n) = \left(\frac{d}{n}\right)\quad\text{for all } n \ge 0,

where $\left(\frac{d}{n}\right)$ is the Kronecker symbol.

This is the character whose $L$ -function appears in Dirichlet's class number formula. It also shows that the hypotheses used in the Dirichlet formula milestones can be satisfied.

Formalization Note The character is a DirichletCharacter ℂ |d|, i.e. a multiplicative character on $\mathbb Z/|d|\mathbb Z$ ; the statement says it agrees with the Kronecker symbol on every natural number.

Preamble

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

Formal statement

namespace ClassNumberFormula

theorem kronecker_is_dirichlet_character (d : ℤ) (hd : IsFundamentalDiscriminant d) :
    ∃ χ : DirichletCharacter ℂ d.natAbs, ∀ n : ℕ, χ n = (kroneckerSymbol d n : ℂ) := 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" ("Let

\chi = (d/m)

be the Kronecker symbol. Then

\chi

is a Dirichlet character."); H. Davenport, Multiplicative Number Theory, 3rd ed., GTM 74, Springer 2000, Ch. 6 (pp. 43–53)

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

For a fundamental discriminant ddd, χ=(d⋅)\chi = \left(\frac{d}{\cdot}\right)χ=(⋅d​) is a Dirichlet character mod ∣d∣|d|∣d∣

For a fundamental discriminant $d$ , $\chi = \left(\frac{d}{\cdot}\right)$ is a Dirichlet character mod $|d|$