English
A nontrivial densely ordered commutative group cannot be cyclic.
Русский
Неп/null образ densely ordered коммутативной группы не может быть циклическим.
LaTeX
$$$\forall \alpha,\ (DenselyOrdered(\alpha) \wedge Nontrivial(\alpha)) \Rightarrow \neg IsCyclic(\alpha)$$$
Lean4
/-- A nontrivial densely linear ordered commutative group can't be a cyclic group. -/
@[to_additive /-- A nontrivial densely linear ordered additive commutative group can't be a cyclic group. -/
]
theorem not_isCyclic_of_denselyOrdered [DenselyOrdered α] [Nontrivial α] : ¬IsCyclic α :=
by
intro h
rcases exists_zpow_surjective α with ⟨a, ha⟩
rcases lt_trichotomy a 1 with hlt | rfl | hlt
· rcases exists_between hlt with ⟨b, hab, hb⟩
rcases ha b with ⟨k, rfl⟩
suffices 0 < k ∧ k < 1 by cutsat
rw [← one_lt_inv'] at hlt
simp_rw [← zpow_lt_zpow_iff_right hlt]
simp_all
· rcases exists_ne (1 : α) with ⟨b, hb⟩
simpa [hb.symm] using ha b
· rcases exists_between hlt with ⟨b, hb, hba⟩
rcases ha b with ⟨k, rfl⟩
suffices 0 < k ∧ k < 1 by cutsat
simp_rw [← zpow_lt_zpow_iff_right hlt]
simp_all
