basisOfIsMaxRank_fundSystem — Mathlib

English

Regulator of the fundamental system equals the regulator of the whole unit group, i.e., regOfFamily (fundSystem K) = regulator K.

Русский

Регулятор фундаментальной системы равен регулятору всей группы единиц: regOfFamily (fundSystem K) = regulator K.

LaTeX

$$$\\mathrm{regOfFamily}(\\mathrm{fundSystem}~K) = \\mathrm{regulator}(K)$$$

Lean4

theorem basisOfIsMaxRank_fundSystem :
    basisOfIsMaxRank (isMaxRank_fundSystem K) = (basisUnitLattice K).ofZLatticeBasis ℝ :=
  by
  ext
  rw [Basis.ofZLatticeBasis_apply, basisOfIsMaxRank_apply, logEmbedding_fundSystem]

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