regulator_eq_det' — Mathlib

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']

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