English
The regulator equals the absolute value of the determinant of a matrix formed from logs of embeddings of a fund system.
Русский
Регулятор равен абсолютному значению детерминанта матрицы, составленной из логарифмов отображений оснований системы.
LaTeX
$$$\\mathrm{regulator}(K) = \\left| \\det \\bigl( \\operatorname{Matrix}.of \\bigl(i \\mapsto \\log w(\\operatorname{fundSystem}(K,i))\\bigr) \\bigr) \\right|$$$
Lean4
theorem regulator_eq_det' :
regulator K = |(Matrix.of fun i ↦ logEmbedding K (Additive.ofMul (fundSystem K ((equivFinRank K).symm i)))).det| :=
by rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det']