dedekindZeta_residue — Mathlib

English

The residue of the Dedekind zeta function at s = 1 is defined to be the expression provided in the previous formula.

Русский

Residue функции Dedekind zeta в точке 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 value of the residue at `s = 1` of the Dedekind zeta function, see
`NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT`.
-/
def dedekindZeta_residue : ℝ :=
  (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * classNumber K) /
    (torsionOrder K * Real.sqrt |discr K|)

Похожие утверждения