linear_ordered_comm_group

Stream: Is there code for X?

[Kevin Buzzard]

We have linear_ordered_comm_field (and semiring and ring) and linear_ordered_add_comm_group but no linear_ordered_comm_group, right?

[Kevin Buzzard]

Is there any reason why one shouldn't make the add_comm_group a to_additiveisation of the comm_group? I am trying to prove that a discrete valuation ring has a valuation, but I'm trying to do it properly :-)

[Johan Commelin]

hmm, not sure why, but I guess it shouldn't be too hard to refactor