regulator_eq_regOfFamily_fundSystem

English

If u is of maximal rank, then regOfFamily u equals ZLattice.covolume of the basis (basisOfIsMaxRank hu).

Русский

Если u имеет максимальный ранг, то regOfFamily u равно ZLattice.covolume базиса basisOfIsMaxRank hu.

LaTeX

$$$regOfFamily u = ZLattice.covolume( span\\mathbb{Z}( basisOfIsMaxRank hu ))$$$

Lean4

theorem regulator_eq_regOfFamily_fundSystem : regulator K = regOfFamily (fundSystem K) := by
  classical
    rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator, ← (basisUnitLattice K).ofZLatticeBasis_span ℝ,
    basisOfIsMaxRank_fundSystem]

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