should SUP INT has OrderedRing?

[Qian Yun]

Currently SUP INT is only Comparable, not OrderedSet.

But I think the current "smaller?" in SUP satisfies
the properties of "<" ?

Is there a reason not to do this?

- Qian

[Waldek Hebisch]

On Sat, Jun 27, 2026 at 05:26:40PM +0800, Qian Yun wrote:
> Currently SUP INT is only Comparable, not OrderedSet.
>
> But I think the current "smaller?" in SUP satisfies
> the properties of "<" ?

Yes, it is implemented in IDPO which for relevant parameters
has OrderedAbelianMonoid.

> Is there a reason not to do this?

Probably nobody cared.

--
Waldek Hebisch