## Stream: maths

### Topic: (non?)commutative linear ordered semirings

#### Johan Commelin (Nov 26 2019 at 15:20):

Question that came up in #1744:

Are there archimedean linearly ordered semirings that are not commutative?

#### Chris Hughes (Nov 26 2019 at 18:40):

I think this works.

Use free_semiring bool and say ff < tt and the free monoid M generated by tt and ff can be linearly ordered lexicographically (I think this is the ordinal 2^omega, short words are always smaller than big words, so not quite the dictionary order). If an indexing set M is linearly ordered, then M ->_0 nat is linearly ordered lexicographically, so you can linearly order the free_semiring (you compare the coefficient of the biggest element of M for which the coefficients differ). I think this satisfies all the axioms, but some of the multiplication ones would be messy to verify. The multiplication axioms for ordered rings seem much simpler than for linear ordered semirings, I'd be quite confident about satisfying those with free_ring bool

#### Johan Commelin (Nov 26 2019 at 20:16):

Ok, funny. Thanks for this example!

Last updated: May 11 2021 at 16:22 UTC