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 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
.
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
.
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
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
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 mul-archimedean group is either isomorphic (and order-isomorphic) to the multiplicative integers, 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.