Dirichlet class number formula, :
OpenClassNumberFormula.dirichlet_class_number_formula_posclass-number-formulanumber-theory
Let be a fundamental discriminant, let be the number of proper (-) equivalence classes of binary quadratic forms of discriminant , let where , is the solution of with minimal, and let be the Dirichlet character modulo given by . Then
This is Dirichlet's class number formula for real quadratic discriminants.
Formalization Note The source PDF prints . With and defined as in the source, that constant is off by a factor : for one has , and , so , while the printed formula gives . The statement here follows Davenport, Multiplicative Number Theory, Ch. 6, the exposition the source says it follows: .
Preamble
import Mathlib import Definitions.Def_ClassNumberFormula_Kronecker import Definitions.Def_ClassNumberFormula_FormClassNumber open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real
Formal statement
namespace ClassNumberFormula
theorem dirichlet_class_number_formula_pos (d : ℤ) (hd : IsFundamentalDiscriminant d)
(hpos : 0 < d) [NeZero d.natAbs] (χ : DirichletCharacter ℂ d.natAbs)
(hχ : ∀ n : ℕ, χ n = (kroneckerSymbol d n : ℂ)) :
(formClassNumber d : ℂ) =
((Real.sqrt d / Real.log (pellEpsilon d) : ℝ) : ℂ) * χ.LFunction 1 := by
sorry
end ClassNumberFormulaSource
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", displayed formula for , case — corrected constant, following H. Davenport, Multiplicative Number Theory, 3rd ed., GTM 74, Springer 2000, Ch. 6 (pp. 43–53)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.