Finite form of for prime conductor
ProvedClassNumberFormula.L_one_finite_form_one_mod_fourclass-number-formulanumber-theory
Let be a prime with , and let be the Dirichlet character modulo given by the Legendre symbol, . Then
Combined with the case of Dirichlet's formula, this gives a finite expression for the class number in terms of logarithms of sines.
Formalization Note The source PDF prints the constant . With the sum over all that constant is off by a factor : for , , while and the printed constant gives half of this. The statement here uses . In the source, with , which equals by quadratic reciprocity.
Preamble
import Mathlib open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real
Formal statement
namespace ClassNumberFormula
theorem L_one_finite_form_one_mod_four (q : ℕ) [Fact q.Prime] (hq : q % 4 = 1)
(χ : DirichletCharacter ℂ q) (hχ : ∀ m : ℕ, χ m = (legendreSym q m : ℂ)) :
χ.LFunction 1 = ((-(1 / Real.sqrt q) * ∑ m ∈ Finset.Ico 1 q,
(legendreSym q m : ℝ) * Real.log (Real.sin (m * π / q)) : ℝ) : ℂ) := 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", last displayed formula, case — corrected constant, see Formalization Note
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.