This project formalizes Holder’s theorem for groups and for semigroups.
Holder’s theorem for groups provides conditions on an ordered group in order to show that it is isomorphic to a subgroup of the real numbers. Similarly, Holder’s theorem for semigroups provides conditions on an ordered semigroup in order to show that it is isomorphic to a subsemigroup of the real numbers.
The formalization of Holder’s theorem for groups is based on the proof in “Groups, Orders, and Dynamics” by Deroin, Navas, and Rivas. The formalization of Holder’s theorem for semigroups is based on the proof in “On ordered semigroups” by N. G. Alimov.
Useful links: