mathlib

afc3f03a - feat(algebra/ordered_group): add linear_ordered_comm_group and linear_ordered_cancel_comm_monoid (#5286)

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) ].