regulator — Mathlib

English

The regulator of a number field K is the covolume of the unit lattice in the real logarithmic space, i.e., the covolume of the z-lattice spanned by the logs of all units.

Русский

Регулятор числа поля K — это ковольюма логарифмического пространства единиц, то есть ковольюма Z-решётки, порождаемой логарифмами всех единиц.

LaTeX

$$$\\mathrm{regulator}(K) = \\mathrm{ZLattice}.\\mathrm{covolume}(\\mathrm{unitLattice}(K))$$$

Lean4

/-- The regulator of a number field `K`. -/
def regulator : ℝ :=
  ZLattice.covolume (unitLattice K)

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