English
For any family u, the regulator regOfFamily u equals the absolute determinant of a matrix built from logs of the embeddings, i.e., regOfFamily u = |det of (log embeddings of u_i)|, up to a choice of index mapping.
Русский
Для любого семейства u регулятор regOfFamily u равен абсолютному определителю матрицы из логарифмов вложений единиц, то есть regOfFamily u = |det( log-вложение (u_i) )|.
LaTeX
$$$\\forall K [Field K] [NumberField K], (u : Fin(\\mathrm{rank} K) \\to (\\mathcal{O}_K)^{\\times}), regOfFamily u = |\\det( of\\, (\\lambda i w : w \\,|\\; w \\neq w' ) \\cdot \\log(u((e i))))|$$$
Lean4
/-- The regulator of a family of units of `K`.
-/
def regOfFamily (u : Fin (rank K) → (𝓞 K)ˣ) : ℝ :=
if hu : IsMaxRank u then ZLattice.covolume (span ℤ (Set.range (basisOfIsMaxRank hu))) else 0
