Commit 2021-01-02 10:18 afc3f03a

feat(algebra/ordered_group): add linear_ordered_comm_group and linear_ordered_cancel_comm_monoid (#5286) We have linear_ordered_add_comm_group but we didn't have linear_ordered_comm_group. This PR adds it, as well as multiplicative versions of canonically_ordered_add_monoid, canonically_linear_ordered_add_monoid and linear_ordered_cancel_add_comm_monoid. I added multiplicative versions of the lemmas about these structures too. The motivation is that I want to slightly generalise the notion of a valuation. [ also random other bits of tidying which I noticed along the way (docstring fixes, adding norm_cast attributes) ].