English
A family u of rank(K) units is of maximal rank if and only if the subgroup generated by these units has finite index in the unit group; equivalently, closure of its range has finite index in the unit lattice.
Русский
Семейство u единиц ранга K максимального ранга тогда и только тогда, когда порождаемая им подгруппа имеет конечный индекс в группе единиц; эквивалентно, замыкание его образа имеет конечный индекс в единичной решётке.
LaTeX
$$$\\forall K [Field K] [NumberField K],\\; (IsMaxRank u) \\iff (closure(\\{u(i) : i \\in Fin (rank K)\\})).FiniteIndex$$$
Lean4
/-- The units of the fundamental system and the torsion of `K` generate the full group of units of `K`.
-/
theorem closure_fundSystem_sup_torsion_eq_top : Subgroup.closure (Set.range (fundSystem K)) ⊔ torsion K = ⊤ :=
by
rw [Subgroup.eq_top_iff', sup_comm]
intro x
obtain ⟨c, rfl, _⟩ := exist_unique_eq_mul_prod K x
exact
Subgroup.mul_mem_sup (SetLike.coe_mem c.1) <|
Subgroup.prod_mem _ fun i _ ↦ Subgroup.zpow_mem _ (Subgroup.subset_closure (Set.mem_range_self i)) _
