English
Let w′ be an infinite place and e an equivalence between {w | w ≠ w′} and Fin(rank K). Then regulator(K) equals the absolute value of a determinant of a matrix whose entries are either mult(w) or mult(w)·log w(fundSystem K (e i)).
Русский
Пусть w′ — бесконечное место и e — равносильность между {w | w ≠ w′} и Fin(rank K). Тогда регулятор(K) равен модулю детерминанта матрицы, элементы которой либо mult(w), либо mult(w)·log w(fundSystem K (e i)).
LaTeX
$$$\\mathrm{regulator}(K) = \\left| \\det \\bigl( \\; (\\mathrm{mult}\\, w) \\;\\text{или}\\; (\\mathrm{mult}\\, w) \\cdot \\log w(\\mathrm{fundSystem}(K,(e i))) \\bigr) \\right|$$$
Lean4
/-- The degree of `K` times the regulator of `K` is equal to the absolute value of the determinant of
the matrix whose columns are `(mult w * log w (fundSystem K i))_i, w` and the column `(mult w)_w`.
-/
theorem finrank_mul_regulator_eq_det (w' : InfinitePlace K) (e : { w // w ≠ w' } ≃ Fin (rank K)) :
finrank ℚ K * regulator K =
|(Matrix.of
(fun i w : InfinitePlace K ↦
if h : i = w' then (w.mult : ℝ) else w.mult * (w (fundSystem K (e ⟨i, h⟩))).log)).det| :=
by rw [regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det]
