English
If a commutative ordered group has a subgroup H with a least element a > 1 in H, then H is generated by a; i.e., H = closure{a}.
Русский
Если подгруппа H в линейно упорядоченной абелевой группе имеет наименьший элемент a > 1, то H порождается этим элементом, то есть H =closure{a}.
LaTeX
$$$ H = \overline{\langle a \rangle}. $$$
Lean4
/-- Given a subgroup `H` of a decidable linearly ordered mul-archimedean abelian group `G`, if there
exists a minimal element `a` of `H ∩ G_{>1}` then `H` is generated by `a`. -/
@[to_additive AddSubgroup.cyclic_of_min /-- Given a subgroup `H` of a decidable linearly ordered
archimedean abelian group `G`, if there exists a minimal element `a` of `H ∩ G_{>0}` then `H` is
generated by `a`. -/
]
theorem cyclic_of_min {H : Subgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a) : H = closure { a } :=
by
obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha
refine le_antisymm ?_ (H.closure_le.mpr <| by simp [a_in])
intro g g_in
obtain ⟨k, ⟨nonneg, lt⟩, _⟩ := existsUnique_zpow_near_of_one_lt a_pos g
have h_zero : g / (a ^ k) = 1 := by
by_contra h
have h : a ≤ g / (a ^ k) := by
refine a_min ⟨?_, ?_⟩
· exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)
· exact lt_of_le_of_ne (by simpa using nonneg) (Ne.symm h)
have h' : ¬a ≤ g / (a ^ k) := not_le.mpr (by simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt)
contradiction
simp [div_eq_one.mp h_zero, mem_closure_singleton]
