finiteIndex_iff_sup_torsion_finiteIndex

English

A family of units has maximal rank if and only if the closure of the subgroup generated by the family has finite index in the full unit group.

Русский

Семейство единиц имеет максимальный ранг тогда и только тогда, когда замыкание подгруппы, порождаемой этим семейством, имеет конечный индекс в полной группе единиц.

LaTeX

$$$\\text{IsMaxRank}(u) \\iff (\\overline{\\langle u \\rangle}).FiniteIndex$$$

Lean4

theorem finiteIndex_iff_sup_torsion_finiteIndex (s : Subgroup (𝓞 K)ˣ) : s.FiniteIndex ↔ (s ⊔ torsion K).FiniteIndex :=
  by
  refine ⟨fun h ↦ Subgroup.finiteIndex_of_le le_sup_left, fun h ↦ ?_⟩
  rw [Subgroup.finiteIndex_iff, ← Subgroup.relIndex_mul_index (le_sup_left : s ≤ s ⊔ torsion K)]
  refine Nat.mul_ne_zero ?_ (Subgroup.finiteIndex_iff.mp h)
  rw [Subgroup.relIndex_sup_left]
  exact Subgroup.FiniteIndex.index_ne_zero

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