Groups with negation and linear order?

Stream: Is there code for X?

[Michael Stoll]

Do we have a structure that captures a (commutative) group with compatible negation (i.e. comm_group and has_distrib_neg) that also carries a linear order that is compatible with this structure?
It is not a linear_ordered_comm_group, since this requires that multiplication with any element preserves the ordering. But here, we have negative elements that reverse the ordering.
Examples of such structures are unit groups of linear_ordered_comm_rings like the multiplicative groups of the real or rational numbers.

[Scott Morrison]

I think we don't.

[Michael Stoll]

Would it make sense to have it?

[Michael Stoll]

(The example I have in mind is unitary (zsqrtd d) for positive non-square d ...)

[Kevin Buzzard]

docs#unitary

[Kevin Buzzard]

I'm confused: how are you ordering units? Are you choosing an embedding?

[Michael Stoll]

When d is a positive nonsquare, ℤ√d has an ordered ring structure: docs#zsqrtd.linear_ordered_comm_ring . I assume this implicitly uses the "standard" real embedding sending the abstract square root to the positive one.
The units are ordered by restriction.

[Michael Stoll]

I was thinking of adding a version of docs#zsqrtd.linear_ordered_comm_ring for integer d, as this seems more natural to me, since the parameter to zsqrtd is an integer.
Or, maybe it would make more sense to refactor this part for integer d rather than adding a version?
I.e., set up a type class pos_nonsquare (which would make sense for elements of an arbitrary ordered semiring, I guess) and use it to replace docs#zsqrtd.nonsquare .
At least for the application (to Pell's equation) that I have in mind, that would be more convenient than the version for natural numbers d.