Commit 2022-01-28 16:51 7e8cb757

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.