mathlib

7e8cb757 - refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for `linear_ordered_comm_group_with_zero` (#7645)

refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for `linear_ordered_comm_group_with_zero` (#7645) This PR continues the refactor of the `ordered` hierarchy, begun in #7371. In this iteration, I weakened the assumptions of the lemmas in `ordered_group`. The bulk of the changes are in the two files * `algebra/ordered_monoid_lemmas` * `algebra/ordered_group` while the remaining files have been edited mostly to accommodate for name/assumption changes. I have tried to be careful to maintain the **exact** assumptions of each one of the `norm_num` and `linarith` lemmas. For this reason, some lemmas have a proof that is simply an application of a lemma with weaker assumptions. The end result is that no lemma whose proof involved a call to `norm_num` or `linarith` broke.