[Merged by Bors] - refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups #2844
Conversation
bryangingechen
added
the
awaiting-review
bryangingechen
changed the title
|
Could you explain what's going on that prevents making the number of primes match up between the additive and multiplicative statements? |
|
The reason for the different number of primes for the multiplicative and additive versions is that I didn't want to change any of the existing names in mathlib. So there would be a statement |
|
I've also fixed conflicts (hopefully). |
| have a + b ≥ a + 0, from add_le_add_left' h, | ||
| by rwa add_zero at this | ||
| @[to_additive le_add_of_nonneg_right'] | ||
| lemma le_mul_of_one_le_right'' (h : 1 ≤ b) : a ≤ a * b := |
There was a problem hiding this comment.
So am I right in thinking that (a) there is no lemma at all called le_mul_of_one_le_right anywhere and (b) there is a lemma called le_mul_of_one_le_right', which is defined in mathlib and used precisely 3 times? So naively one might say that we could rename current le_mul_of_one_le_right' to le_mul_of_one_le_right and then rename this to le_mul_of_one_le_right'?
But actually current le_mul_of_one_le_right'is a lemma about semirings and should arguably be called le_mul_of_nonneg_of_one_le_right.
Edit: I see now I've looked at the rest of the PR that there seem to be too many unbalanced ' issues here for it to be worth fixing them all at once.
| have 0 + a ≤ b + a, from add_le_add_right' h, | ||
| by rwa zero_add at this | ||
| @[to_additive le_add_of_nonneg_left'] | ||
| lemma le_mul_of_one_le_left'' (h : 1 ≤ b) : a ≤ b * a := |
There was a problem hiding this comment.
There is no le_mul_of_one_le_left, and the lemma le_mul_of_one_le_left' is defined in src/algebra and then never used at all! Again it's about semirings and could be renamed le_mul_of_nonneg_of_one_le_left. (did we decide that "left" meant "the left one is not the duplicated one"?
(Edit: maybe just don't bother)
| lemma add_nonneg' (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b := | ||
| le_add_of_nonneg_of_le' ha hb | ||
| @[to_additive add_nonneg'] | ||
| lemma one_le_mul' (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b := |
| lemma add_pos_of_pos_of_nonneg' (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b := | ||
| lt_of_lt_of_le ha $ le_add_of_nonneg_right' hb | ||
| @[to_additive] | ||
| lemma mul_one_lt_of_one_lt_of_one_le' (ha : 1 < a) (hb : 1 ≤ b) : 1 < a * b := |
There was a problem hiding this comment.
If you're happy with this name (and why not?) then maybe le_mul_of_nonneg_of_one_le_right is OK (above)?
| lemma monotone.add (hf : monotone f) (hg : monotone g) : monotone (λ x, f x + g x) := | ||
| λ x y h, add_le_add' (hf h) (hg h) | ||
| @[to_additive monotone.add] | ||
| lemma monotone.mul' (hf : monotone f) (hg : monotone g) : monotone (λ x, f x * g x) := |
There was a problem hiding this comment.
monotone.mul is defined and then never used, and could be monotone.mul_of_nonneg
| left_cancel_monoid α := { ..‹ordered_cancel_comm_monoid α› } | ||
|
|
||
| @[to_additive add_le_add_left] | ||
| lemma mul_le_mul_left'' : ∀ {a b : α} (h : a ≤ b) (c : α), c * a ≤ c * b := |
There was a problem hiding this comment.
OK I am beginning to tire of this :-( I can see the problem now. add_le_add_left is used all over the place, and is a theorem about add comm monoids, and mul_le_mul_left is a theorem about semirings. I'm not sure it's possible to keep the primes matched up without a major amount of hassle for what is basically a small gain.
|
|
||
| @[to_additive] | ||
| lemma mul_le_mul_three {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : | ||
| a * b * c ≤ d * e * f := |
There was a problem hiding this comment.
I thought they liked
le_trans (mul_le_mul'' (mul_le_mul'' h₁ h₂) h₃) $ le_refl _
better?
There was a problem hiding this comment.
wait -- whatever is le_trans even doing there? mul_le_mul'' (mul_le_mul'' h₁ h₂) h₃?
src/algebra/ordered_group.lean
Outdated
| TODO: | ||
| The `add_lt_add_left` field of `ordered_add_comm_group` is redundant, | ||
| and it is no longer in core so we can remove it now. | ||
| This alternative constructor is the best we could do. |
There was a problem hiding this comment.
Surely ... "is a workaround until someone fixes this"?
There was a problem hiding this comment.
I guess change "best we can do" to "best we could do" is not very strong wording (-;
|
@jcommelin, I propose we don't worry about the inconsistent primes, as this is still a step in the right direction, and merge (after resolving conflicts), as is. |
|
bors d+ |
|
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
github-actions
bot
added
ready-to-merge
…onoids/groups (#2844) This PR defines multiplicative versions of ordered monoids and groups. It also lints the file.
|
Build failed: |
bryangingechen
removed
the
ready-to-merge
|
sudo bors merge |
github-actions
bot
added
the
ready-to-merge
…onoids/groups (#2844) This PR defines multiplicative versions of ordered monoids and groups. It also lints the file.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…onoids/groups (leanprover-community#2844) This PR defines multiplicative versions of ordered monoids and groups. It also lints the file.
This PR defines multiplicative versions of ordered monoids and groups. It also lints the file.