Theorems · Theorem · order theory

LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered

∀ (G : Type u_2) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G],
  Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic) to the integers, or is densely ordered, exclusively. (See also LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered.)

Defined in

Mathlib.GroupTheory.ArchimedeanDensely

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean