Theorems · Theorem · order theory

LinearOrderedCommGroup.discrete_iff_not_denselyOrdered

∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G],
  Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic) to the multiplicative integers, or is densely ordered, exclusively. (See also LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered.)

Defined in

Mathlib.GroupTheory.ArchimedeanDensely

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupLinearOrderIsOrderedMonoidMulArchimedean