## Stream: Is there code for X?

### Topic: linear_ordered_comm_group

#### Kevin Buzzard (Nov 20 2020 at 19:59):

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 (Nov 20 2020 at 20:01):

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 (Nov 20 2020 at 20:12):

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

Last updated: May 16 2021 at 05:21 UTC