Theorems · Definition · order theory

LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos

{G : Type u_2} →
  [inst : AddCommGroup G] →
    [inst_1 : LinearOrder G] → [IsOrderedAddMonoid G] → [Archimedean G] → {x : G} → IsLeast {y | 0 < y} x → G ≃+o ℤ

If an element of a linearly ordered archimedean additive group is the least positive element, then the whole group is isomorphic (and order-isomorphic) to the integers.

Defined in

Mathlib.GroupTheory.ArchimedeanDensely

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean