chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace without_zero_le_one
#16525
Conversation
…e namespace `without_zero_le_one` The fourth part of #16449 There are still some useless lemmas which were simply ported from `algebra/order/monoid_lemmas`, this PR removes them. Also some lemmas have both assumptions like `1 < a` `0 < a`, this is because the file does not use type classes like `zero_le_one_class` currently. So I put these lemmas in the namespace `without_zero_le_one`.
FR-vdash-bot
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
YaelDillies
added
the
merge-conflict
FR-vdash-bot
removed
the
merge-conflict
src/algebra/order/ring_lemmas.lean
Outdated
| lemma mul_le_of_le_one_left [mul_pos_mono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b := | ||
| by simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb | ||
| lemma mul_le_of_le_one_right [pos_mul_mono α] (a0 : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a := | ||
| by simpa only [mul_one] using mul_le_mul_of_nonneg_left h a0 | ||
|
|
||
| lemma le_mul_of_one_le_left [mul_pos_mono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b := | ||
| by simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb | ||
| lemma le_mul_of_one_le_right [pos_mul_mono α] (a0 : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b := | ||
| by simpa only [mul_one] using mul_le_mul_of_nonneg_left h a0 | ||
|
|
||
| lemma mul_le_of_le_one_right [pos_mul_mono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a := | ||
| by simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha | ||
| lemma mul_le_of_le_one_left [mul_pos_mono α] (b0 : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b := | ||
| by simpa only [one_mul] using mul_le_mul_of_nonneg_right h b0 |
There was a problem hiding this comment.
Why did you swap the orders of these? It just makes the diff a lot bigger.
There was a problem hiding this comment.
(also as a LTR language, I would expect the left lemmas to come before the right lemmas anyway)
There was a problem hiding this comment.
This order is consistent with the previous lemmas in the file. Also the order of their typeclass assumptions is consistent with the conventions in this file.
FR-vdash-bot
changed the title
without_zero_le_onewithout_zero_le_one
|
Do we actually need the lemmas in |
|
These can be dumped currently, but I'm thinking of strengthening these lemmas by using |
YaelDillies
added
awaiting-author
FR-vdash-bot
added
awaiting-review
|
Could you explain what your definition of "useless lemma" is in the PR description and either
|
|
"useless lemmas" is what you mentioned in doc-string and lemmas whose assumptions imply
These lemmas were simply ported from I made PR #18158 to add |
|
I know what I meant. I'm just asking you to let everyone else know by putting it in the PR description 😄 |
eric-wieser
added
the
not-too-late
|
Can you please fix the conflict? |
kim-em
added
awaiting-author
FR-vdash-bot
added
awaiting-review
github-actions
bot
added
modifies-synchronized-file
|
@YaelDillies, could you comment on this PR? What remains to be done? |
|
Closing, since this was ported to leanprover-community/mathlib4#9250 |
YaelDillies
removed
awaiting-review
The fourth part of #16449
There are still some useless lemmas that were simply ported from
algebra/order/monoid_lemmas, this PR removes them. "useless lemmas" are lemmas that just chain an existing lemma with an assumption and lemmas whose assumptions imply1 ≤ 0. These lemmas were simply ported fromalgebra/order/monoid_lemmas.Also, some lemmas have both assumptions like
1 < a0 < a, this is because the file does not use type classes likezero_le_one_classcurrently. This PR puts these lemmas in the namespacewithout_zero_le_one.mathlib4: leanprover-community/mathlib4#782