[Merged by Bors] - feat: port algebra.order.monoid.lemmas#608
[Merged by Bors] - feat: port algebra.order.monoid.lemmas#608
Conversation
|
Note the existing Mathlib.Algebra.Order.MonoidLemmas as well |
Yes, I cannibalized the ~10 lemmas ported there (but didn't yet incorporate the deletion of that file into this PR -- I will when everything else is ready). |
|
@hrmacbeth, why is this marked as depending on #591 ( |
|
Oh, I see, you need to add the import still! |
| (h₁ : a < b) (h₂ : c < d) : | ||
| a * c < b * d := |
There was a problem hiding this comment.
| (h₁ : a < b) (h₂ : c < d) : | |
| a * c < b * d := | |
| (h₁ : a < b) (h₂ : c < d) : a * c < b * d := |
We could save a line here like this (I've been doing this, giving no special preference for a new line after :), but it's not important. (And eventually an automatic reformatter may take care of all this.)
There was a problem hiding this comment.
Just to check, is the situation that mathlib is agnostic on newline after :?
Or is there a preference for newline after : but it's not worth enforcing it here because it's not provided by mathport output and there might be an automatic reformatter someday?
Or is there a preference for no newline after :?
There was a problem hiding this comment.
Preference for no newline after :. (But slight preference for after the colon rather than in the midst of arguments or in the middle of the return type.)
|
Looks great, besides the unfortunately tedious problem with #aligns for |
|
bors merge |
I had to change one proof due to a `to_additive` issue, see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20thinks.20it's.20in.20a.20namespace). mathlib3 sha: 7cca171008afb30576d2d4c51173700a780c23d0 [Diff from mathport output](https://github.com/leanprover-community/mathlib4/compare/40d48abdfdf951c6dc1cb7681de7fb46156a0039..hrmacbeth-algebra-monoid-lemmas) - [x] depends on: #591
|
Pull request successfully merged into master. Build succeeded: |
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * leanprover-community/mathlib4#563 * leanprover-community/mathlib4#608 * leanprover-community/mathlib4#627 * leanprover-community/mathlib4#638 * leanprover-community/mathlib4#641 * leanprover-community/mathlib4#645 * leanprover-community/mathlib4#650
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * leanprover-community/mathlib4#563 * leanprover-community/mathlib4#608 * leanprover-community/mathlib4#627 * leanprover-community/mathlib4#638 * leanprover-community/mathlib4#641 * leanprover-community/mathlib4#645 * leanprover-community/mathlib4#650
I had to change one proof due to a
to_additiveissue, see Zulip.mathlib3 sha: 7cca171008afb30576d2d4c51173700a780c23d0
Diff from mathport output