Finite form of $L(1,\chi)$ for prime conductor $q\equiv3\pmod 4$

Proved

ClassNumberFormula.L_one_finite_form_three_mod_four

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

class-number-formulanumber-theory

Let $q$ be a prime with $q\equiv 3\pmod 4$ , and let $\chi$ be the Dirichlet character modulo $q$ given by the Legendre symbol, $\chi(m) = \left(\frac{m}{q}\right)$ . Then

L(1,\chi) = -\frac{\pi}{q^{3/2}}\sum_{m=1}^{q-1} m\left(\frac{m}{q}\right).

Combined with the case $d=-q$ of Dirichlet's formula, this gives a finite expression for the class number.

Formalization Note In the source, $\chi = \left(\frac{d}{\cdot}\right)$ is primitive with prime conductor $q$ , so $d = -q$ , and by quadratic reciprocity $\chi(m) = \left(\frac{m}{q}\right)$ ; the statement uses this explicit description. $L(1,\chi)$ is Mathlib's DirichletCharacter.LFunction at $s=1$ .

Preamble

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

Formal statement

namespace ClassNumberFormula

theorem L_one_finite_form_three_mod_four (q : ℕ) [Fact q.Prime] (hq : q % 4 = 3)
    (χ : DirichletCharacter ℂ q) (hχ : ∀ m : ℕ, χ m = (legendreSym q m : ℂ)) :
    χ.LFunction 1 = ((-(π / (q : ℝ) ^ ((3 : ℝ) / 2)) *
      ∑ m ∈ Finset.Ico 1 q, (m : ℝ) * (legendreSym q m : ℝ) : ℝ) : ℂ) := 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", last displayed formula, case

q \equiv 3 \pmod 4

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

Finite form of L(1,χ)L(1,\chi)L(1,χ) for prime conductor q≡3(mod4)q\equiv3\pmod 4q≡3(mod4)

Finite form of $L(1,\chi)$ for prime conductor $q\equiv3\pmod 4$