English
For any infinite place w′, regulator equals the determinant of a matrix with entries mult(w)·log w(fundSystem K i) for w ≠ w′.
Русский
Для произвольного бесконечного место w′ регулятор равен детерминанту матрицы со степенями mult(w)·log w(fundSystem K i) по всем w ≠ w′.
LaTeX
$$$\\mathrm{regulator}(K) = \\left| \\det \\bigl( \\mathrm{Matrix.of} \\bigl( i,w: \\{ w \\;\\vert\\; w \\neq w' \\} \\mapsto (\\mathrm{mult}\\ w) \\cdot \\log w(\\mathrm{fundSystem}(K,(e\,i))) \\bigr) \\bigr) \\right|$$$
Lean4
/-- For any infinite place `w'`, the regulator is equal to the absolute value of the determinant
of the matrix with entries `(mult w * log w (fundSystem K i))_i` for `w ≠ w'`.
-/
theorem regulator_eq_det (w' : InfinitePlace K) (e : { w // w ≠ w' } ≃ Fin (rank K)) :
regulator K =
|(Matrix.of fun i w : { w // w ≠ w' } ↦ (mult w.val : ℝ) * Real.log (w.val (fundSystem K (e i) : K))).det| :=
by rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det]
