English
Let G be a linearly ordered commutative group with zero, nontrivial. Then either G is congruent to ℤᵐ⁰ as an ordered group, or the order is densely ordered.
Русский
Пусть G — линейно упорядоченная коммутативная группа с нулем, не тривиальная. Тогда либо G ≅ ℤᵐ⁰ как упорядоченная группа, либо порядок плотный.
LaTeX
$$$\exists \phi: G \cong_o \mathbb{Z}^{\mathbf{m0}} \;\lor\; \mathrm{DenselyOrdered}(G)$$$
Lean4
/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
either isomorphic (and order-isomorphic) to `ℤᵐ⁰`, or is densely ordered. -/
theorem discrete_or_denselyOrdered (G : Type*) [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] :
Nonempty (G ≃*o ℤᵐ⁰) ∨ DenselyOrdered G := by
classical
rw [← denselyOrdered_units_iff]
refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp_left ?_
intro ⟨f⟩
exact ⟨OrderMonoidIso.withZeroUnits.symm.trans f.withZero⟩
