Theorems · Theorem · order theory

LinearOrderedAddCommGroup.discrete_or_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.

Defined in

Mathlib.GroupTheory.ArchimedeanDensely

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean