IsOrderedRing for AddMonoidAlgebra

Stream: Is there code for X?

[Violeta Hernández]

Just making sure I'm not missing something. We haven't yet defined lexicographic/colexicographic orderings on docs#AddMonoid algebra, or have we?

[Violeta Hernández]

I wanted to use this in the CGT repo to define the Cantor normal form on NatOrdinal (ordinals with Hessenberg operations) as an isomorphism NatOrdinal ≃+*o Colex ℕ[NatOrdinal]

[Yaël Dillies]

No indeed I don't think we have that