English
If g1 and g2 are elements with g1 < 1, g2 < 1 and Subgroup.zpowers g1 = Subgroup.zpowers g2, then g1 = g2.
Русский
Если g1 < 1 и g2 < 1 и Subgroup.zpowers g1 = Subgroup.zpowers g2, то g1 = g2.
LaTeX
$$$g_1<1 \land g_2<1 \land (Subgroup.zpowers g_1)=(Subgroup.zpowers g_2) \Rightarrow g_1=g_2$$$
Lean4
theorem genLTOne_unique_of_zpowers_eq {g1 g2 : G} (hg1 : g1 < 1) (hg2 : g2 < 1)
(h : Subgroup.zpowers g1 = Subgroup.zpowers g2) : g1 = g2 :=
by
rcases (Subgroup.zpowers g2).bot_or_nontrivial with (h' | h')
· rw [h'] at h
simp_all only [Subgroup.zpowers_eq_bot]
· have h1 : IsCyclic ↥(Subgroup.zpowers g2) := by rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]; use g2
have h2 : Nontrivial ↥(Subgroup.zpowers g1) := by rw [h]; exact h'
have h3 : IsCyclic ↥(Subgroup.zpowers g1) := by rw [h]; exact h1
simp only [(Subgroup.zpowers g2).genLTOne_unique hg1 h]
simp only [← h]
simp only [(Subgroup.zpowers g1).genLTOne_unique hg2 h.symm]
