[Merged by Bors] - feat(algebra/order/monoid_lemmas_zero_lt): port some lemmas from algebra.order.monoid_lemmas
#12961
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ebra.order.monoid_lemmas` Although the names of these lemmas are from `algebra.order.monoid_lemmas`, many of the lemmas in `algebra.order.monoid_lemmas` have incorrect names, and some others may not be appropriate. Also, many lemmas are missing in `algebra.order.monoid_lemmas`. It may be necessary to make some renames and additions.
negiizhao
added
the
awaiting-review
negiizhao
commented
Mar 26, 2022
| -- proven with `a0 : 0 ≤ a` as `mul_le_of_le_one_right'` | ||
| lemma mul_le_of_le_one_right [pos_mul_mono α] {a b : α} (h : b ≤ 1) (a0 : 0 < a) : | ||
| a * b ≤ a := | ||
| mul_le_of_le_of_le_one le_rfl h a0 |
There was a problem hiding this comment.
This name is from algebra.order.monoid_lemmas. But I'm wondering if it might be inappropriate.
There was a problem hiding this comment.
I suggest opening a separate PR for this issue, in case you actually want to change the name of this lemma. Already as is, this PR is very long and will take time to review.
|
I'm leaving here a comment that I made privately to FR. This way, it stays in the PR trail. One quick comment is that you mention the typeclass assumptions in each lemma, while most of the times, lemmas with the same typeclass assumptions are grouped together. I'm not necessarily asking to change it, but I think that it is more standard to have sections with uniform typeclass assumptions. I do not necessarily insist on this kind of grouping, but someone else might have a more conceptual preference. |
|
My current approach is to sort by algebraic assumptions and order assumptions first, then put similar lemmas together. This approach might avoid missing lemmas, and one can figure out similar lemmas at the same time while reading. However, the grouped lemmas may not have the same co(ntra)variant typeclass assumptions. So (only) co(ntra)variant typeclass assumptions might be mentioned in each lemma. |
|
I am happy with either approach: sections with uniform typeclass assumptions, or similar looking lemmas grouped together. If someone else has a strong preference, they can say so. |
adomani
approved these changes
Apr 6, 2022
leanprover-community-bot-assistant
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Apr 9, 2022
…ebra.order.monoid_lemmas` (#12961) Although the names of these lemmas are from `algebra.order.monoid_lemmas`, many of the lemmas in `algebra.order.monoid_lemmas` have incorrect names, and some others may not be appropriate. Also, many lemmas are missing in `algebra.order.monoid_lemmas`. It may be necessary to make some renames and additions.
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Apr 9, 2022
…ebra.order.monoid_lemmas` (#12961) Although the names of these lemmas are from `algebra.order.monoid_lemmas`, many of the lemmas in `algebra.order.monoid_lemmas` have incorrect names, and some others may not be appropriate. Also, many lemmas are missing in `algebra.order.monoid_lemmas`. It may be necessary to make some renames and additions.
|
This PR was included in a batch that was canceled, it will be automatically retried |
bors bot
pushed a commit
that referenced
this pull request
Apr 9, 2022
…ebra.order.monoid_lemmas` (#12961) Although the names of these lemmas are from `algebra.order.monoid_lemmas`, many of the lemmas in `algebra.order.monoid_lemmas` have incorrect names, and some others may not be appropriate. Also, many lemmas are missing in `algebra.order.monoid_lemmas`. It may be necessary to make some renames and additions.
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Apr 10, 2022
…ebra.order.monoid_lemmas` (#12961) Although the names of these lemmas are from `algebra.order.monoid_lemmas`, many of the lemmas in `algebra.order.monoid_lemmas` have incorrect names, and some others may not be appropriate. Also, many lemmas are missing in `algebra.order.monoid_lemmas`. It may be necessary to make some renames and additions.
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Apr 10, 2022
…ebra.order.monoid_lemmas` (#12961) Although the names of these lemmas are from `algebra.order.monoid_lemmas`, many of the lemmas in `algebra.order.monoid_lemmas` have incorrect names, and some others may not be appropriate. Also, many lemmas are missing in `algebra.order.monoid_lemmas`. It may be necessary to make some renames and additions.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
algebra.order.monoid_lemmasalgebra.order.monoid_lemmas
bors bot
pushed a commit
that referenced
this pull request
Sep 14, 2022
…16447) `pos_mul_mono`/`mul_pos_mono` and `pos_mul_reflect_lt`/`mul_pos_reflect_lt` were stated as covariance/contravariance of `{x : α // 0 < α}` over `α` even though the extension to `{x : α // 0 ≤ α}` also holds. This meant that many lemmas were relying on antisymmetry only to treat the cases `a = 0` and `0 < a` separately, which made them need `partial_order` and depend on `classical.choice`. This prevented #16172 from actually removing the `decidable` lemma in `algebra.order.ring` after #16189 got merged. Further, #16189 did not actually get rid of the temporary `zero_lt` namespace, so name conflicts that arise were not fixed. Finally, `le_mul_of_one_le_left` and its seven friends were reproved inline about five time each. Hence in this PR we * restate `pos_mul_mono`, `mul_pos_mono`, `pos_mul_reflect_lt`, `mul_pos_reflect_lt` using `{x : α // 0 ≤ α}` * provide the (classical) equivalence with the previous definitions in a `partial_order`. * generalise lemmas from `partial_order` to `preorder`. * delete all lemmas in the `preorder` namespace as they are now fully generalized. This in essence reverts (parts of) #12961, #13296 and #13299. * replace most of the various `has_le`/`has_lt` assumptions by a blank `preorder` one, hence simplifying the file sectioning * remove the `zero_lt` namespace. * rename lemmas to fix name conflicts. * delete a few lemmas that were left in `algebra.order.ring`. * golf proofs involving `le_mul_of_one_le_left` and its seven friends. This is why the PR has a -450 lines diff.
b-mehta
pushed a commit
that referenced
this pull request
Sep 21, 2022
…16447) `pos_mul_mono`/`mul_pos_mono` and `pos_mul_reflect_lt`/`mul_pos_reflect_lt` were stated as covariance/contravariance of `{x : α // 0 < α}` over `α` even though the extension to `{x : α // 0 ≤ α}` also holds. This meant that many lemmas were relying on antisymmetry only to treat the cases `a = 0` and `0 < a` separately, which made them need `partial_order` and depend on `classical.choice`. This prevented #16172 from actually removing the `decidable` lemma in `algebra.order.ring` after #16189 got merged. Further, #16189 did not actually get rid of the temporary `zero_lt` namespace, so name conflicts that arise were not fixed. Finally, `le_mul_of_one_le_left` and its seven friends were reproved inline about five time each. Hence in this PR we * restate `pos_mul_mono`, `mul_pos_mono`, `pos_mul_reflect_lt`, `mul_pos_reflect_lt` using `{x : α // 0 ≤ α}` * provide the (classical) equivalence with the previous definitions in a `partial_order`. * generalise lemmas from `partial_order` to `preorder`. * delete all lemmas in the `preorder` namespace as they are now fully generalized. This in essence reverts (parts of) #12961, #13296 and #13299. * replace most of the various `has_le`/`has_lt` assumptions by a blank `preorder` one, hence simplifying the file sectioning * remove the `zero_lt` namespace. * rename lemmas to fix name conflicts. * delete a few lemmas that were left in `algebra.order.ring`. * golf proofs involving `le_mul_of_one_le_left` and its seven friends. This is why the PR has a -450 lines diff.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Although the names of these lemmas are from
algebra.order.monoid_lemmas, many of the lemmas inalgebra.order.monoid_lemmashave incorrect names, and some others may not be appropriate. Also, many lemmas are missing inalgebra.order.monoid_lemmas. It may be necessary to make some renames and additions.