dedekindZeta_residue_def — Mathlib

English

Explicitly states the equality of dedekindZeta_residue with the product formula described previously.

Русский

Явно формулируется равенство dedekindZeta_residue с формулой произведения.

LaTeX

$$$\mathrm{dedekindZeta\_residue}(K) = (2^ {nrRealPlaces(K)} (2\pi)^{nrComplexPlaces(K)} \mathrm{regulator}(K) \mathrm{classNumber}(K)) / (\mathrm{torsionOrder}(K) \sqrt{|\mathrm{discr}(K)|})$$$

Lean4

theorem dedekindZeta_residue_def :
    dedekindZeta_residue K =
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * classNumber K) /
        (torsionOrder K * Real.sqrt |discr K|) :=
  rfl

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