English
For any cyclic subgroup H of G, the element g with g < 1 is unique, i.e. if g < 1 and Subgroup.zpowers g = H, then g is the same as the canonical generator H.genLTOne.
Русский
Для любой циклической подгруппы H в G элемент g с g < 1 уникален: если g < 1 и Subgroup.zpowers g = H, то g равно каноническому генератору H.genLTOne.
LaTeX
$$$\forall g\,(g<1)\land (Subgroup.zpowers g=H)\Rightarrow g=H.genLTOne$$$
Lean4
theorem genLTOne_unique {g : G} (hg : g < 1) (hH : Subgroup.zpowers g = H) : g = H.genLTOne :=
by
have hg' : ¬IsOfFinOrder g := not_isOfFinOrder_of_isMulTorsionFree (ne_of_lt hg)
rw [← H.genLTOne_zpowers_eq_top] at hH
rcases (Subgroup.zpowers_eq_zpowers_iff hg').mp hH with _ | h
· assumption
rw [← one_lt_inv', h] at hg
exact (not_lt_of_gt hg <| Subgroup.genLTOne_lt_one _).elim
