Linearly ordered group
From Wikipedia, the free encyclopedia
In abstract algebra a linearly ordered or totally ordered group is an ordered group G such that the order relation "
" is total. This means that the following statements hold for all 
:
- if
and 
then a = b (antisymmetry) - if and
then 
(transitivity) - or (totality)
- the order relation is translation invariant: if then
and 
.
In analogy with ordinary numbers, we call an element c of an ordered group positive if 
. The set of positive elements in a group is often denoted with G + . For every element a of a linearly ordered group G either 
, or 
, or a = 0 [1]. If a linearly ordered group G is not trivial (i.e. 0 is not its only element), then G + is infinite. Therefore, every nontrivial linearly ordered group is infinite [2].
If a is an element of a linearly ordered group G, then the absolute value of a, denoted by | a | , is defined to be:
If in addition the group G is abelian, then for any 
the triangle inequality is satisfied: 
[3].
Otto Hölder showed that every linearly ordered group satisfying an Archimedean property is isomorphic to a subgroup of the additive group of real numbers.
The names below refer to the theorems formally verified by the IsarMathLib project.
