Formalization of Holder's Theorem for semigroups (and for groups).
Here is more information on the project. That page also link to the the blueprint and the documentation for the project.
The formalization follows the paper "On ordered semigroups" by N.G. Alimov and "Groups, Orders, and Dynamics" by Deroin, Navas, and Rivas.