Holder's Theorem for Groups #
This file contains the proof of Holder's theorem for groups.
theorem
holders_theorem
{α : Type u}
[Group α]
[LinearOrder α]
[IsLeftOrderedSemigroup α]
(arch : archimedean_group α)
:
∃ (G : Subgroup (Multiplicative ℝ)), Nonempty (α ≃*o ↥G)
Every left linear ordered group that is Archimedean
is monoid order isomorphic to a subgroup of ℝ.