English
The Dedekind zeta residue at s = 1 is given by the standard product of geometric invariants: residues depend on regulator, class number, discriminant, and torsion, via a specific rational expression.
Русский
Предел резидуа Дедекенд–зета в s = 1 задаётся стандартной комбинацией инфор-маций: регулятор, число класса, дискриминант и торсионные участки через заданное выражение.
LaTeX
$$$\mathrm{dedekindZeta\_residue}(K) = \dfrac{2^{nrRealPlaces(K)} (2\pi)^{nrComplexPlaces(K)} \mathrm{regulator}(K) \mathrm{classNumber}(K)}{\mathrm{torsionOrder}(K) \sqrt{|\mathrm{discr}(K)|}}$$$
Lean4
/-- The Dedekind zeta function of a number field. It is defined as the `L`-series with coefficients
the number of integral ideals of norm `n`.
-/
def dedekindZeta (s : ℂ) :=
LSeries (fun n ↦ Nat.card { I : Ideal (𝓞 K) // absNorm I = n }) s
