Holders Theorem for Semigroups and Groups

Stream: general

[Eric Paul]

I wanted to share this project I've finished of formalizing Holders Theorem for semigroups and groups!

As a quick summary, the two theorems provide conditions to show that an ordered semigroup/group is isomorphic to a subsemigroup/subgroup of the real numbers.

I had a lot of fun working on it. Also, I'd be happy to help add any parts of it that seem relevant to mathlib. And thanks to @Tomas Ortega for help formalizing parts of it!

[Ruben Van de Velde]

Planning to contribute it to mathlib?

[Yaël Dillies]

cc @Bhavik Mehta who asked me about this recently

[Eric Paul]

Ruben Van de Velde said:

Planning to contribute it to mathlib?

That's my hope! I'll make a topic about it in the mathlib channel.