English
In a nontrivial densely ordered commutative group, the integer powers of an element cannot be dense in the whole group.
Русский
В ненулевой плотно упорядоченной коммутативной группе целочисленные степени элемента не могут образовывать плотное множество в группе.
LaTeX
$$$\neg\, \mathrm{DenseRange}(a^{\cdot}: \mathbb{Z} \to G).$$$
Lean4
/-- In a nontrivial densely linearly ordered commutative group,
the integer powers of an element can't be dense. -/
@[to_additive /-- In a nontrivial densely linearly ordered additive group,
the integer multiples of an element can't be dense. -/
]
theorem not_denseRange_zpow [Nontrivial G] [DenselyOrdered G] {a : G} : ¬DenseRange (a ^ · : ℤ → G) :=
denseRange_zpow_iff_surjective.not.mpr fun h ↦ not_isCyclic_of_denselyOrdered G ⟨⟨a, h⟩⟩
