Commit 2022-08-24 21:27 62740866
View on Github →refactor(algebra/order/{monoid_lemmas_zero_lt + ring} + crumbs) remove duplicate lemmas (#16189)
This is one of the cleaning up stages of the order refactor. This PR removes some of the lemmas for ordered semirings that are now superfluous.
To keep things simple, the new lemmas are in the zero_lt namespace and we export this namespace. Probably, this will not stay this way once the tide of unsuccessful builds washes away.
The plan for this PR is to align names and order of explicit hypotheses in the zero_lt file with the lemmas in ring, in order to delete them. This will likely involve changing a few extra files, but I'm hoping to seriously contain the diff outside of these two files.
I want to thank @negiizhao who has been a great help in taking over and pushing forward the refactor!