English
Let H be a cyclic subgroup of a linearly ordered commutative group G. Then there exists an element g ∈ H with g < 1 that generates H, i.e. H = ⟨g⟩.
Русский
Пусть H — циклическая подгруппа линейно упорядоченной коммутативной группы G. Тогда существует элемент g ∈ H, такой что g < 1, и эта подгруппа порождается элементом g: H = ⟨g⟩.
LaTeX
$$$\exists g \in H\; (g < 1) \quad\text{and}\quad H = \langle g \rangle$$$
Lean4
/-- Given a subgroup of a cyclic linearly ordered commutative group, this is a generator of
the subgroup that is `< 1`. -/
@[to_additive negGen /-- Given an additive subgroup of an additive cyclic linearly ordered
commutative group, this is a negative generator of the subgroup. -/
]
protected noncomputable def genLTOne : G :=
H.exists_generator_lt_one.choose
