Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC