Documentation

Mathlib.GroupTheory.ArchimedeanDensely

Archimedean groups are either discrete or densely ordered #

This file proves a few additional facts about linearly ordered additive groups which satisfy the Archimedean property -- they are either order-isomorphic and additvely isomorphic to the integers, or they are densely ordered.

They are placed here in a separate file (rather than incorporated as a continuation of GroupTheory.Archimedean) because they rely on some imports from pointwise lemmas.

The subgroup generated by an element of a group equals the set of integer powers of the element, such that each power is a unique element. This is the stronger version of Subgroup.mem_closure_singleton.

The additive subgroup generated by an element of an additive group equals the set of integer multiples of the element, such that each multiple is a unique element. This is the stronger version of AddSubgroup.mem_closure_singleton.

In two linearly ordered groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    In two linearly ordered additive groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        If an element of a linearly ordered mul-archimedean group is the least element greater than 1, then the whole group is isomorphic (and order-isomorphic) to the multiplicative integers.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

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

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

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

          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.

          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, exclusively