This repository was archived by the owner on Jul 24, 2024. It is now read-only.
[Merged by Bors] - move(algebra/order/monoid/*): relocate zero_le_one_class again#17820
Closed
astrainfinita wants to merge 2 commits intomasterfrom
Closed
[Merged by Bors] - move(algebra/order/monoid/*): relocate zero_le_one_class again#17820astrainfinita wants to merge 2 commits intomasterfrom
zero_le_one_class again#17820astrainfinita wants to merge 2 commits intomasterfrom
Conversation
zero_le_one_class againzero_le_one_class again
Member
|
This PR changes the typeclass assumptions (as discussed on Zulip) too right? Please make sure the PR description mentions that! |
Collaborator
Author
|
Oh, I forgot that, there it is now. |
Closed
2 tasks
Collaborator
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Dec 6, 2022
) #17646 move `zero_le_one_class` to `algebra.order.monoid.with_zero`. This PR split things about `zero_le_one_class` into two files. Also, all lemmas about numerics other than 0 and 1 require typeclass `add_monoid_with_one` now. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/OfNat)
|
Pull request successfully merged into master. Build succeeded: |
zero_le_one_class againzero_le_one_class again
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Dec 6, 2022
mathlib3 SHA: dad7ecf9a1feae63e6e49f07619b7087403fb8d4 Ports Algebra.Order.Monoid.WithZero.[Defs, Basic]. - [x] depends on #841 - [x] depends on leanprover-community/mathlib3#17820 I'm planning to wait until leanprover-community/mathlib3#17820 is approved before doing a final refactor to move lemmas where they're needed. Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me>
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Dec 7, 2022
Ported by hand from current mathlib: 07fee0ca54c320250c98bacf31ca5f288b2bcbe2 This is thoroughly ridiculous, but it my fault for merging leanprover-community/mathlib3#17820, see discussion on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/OfNat). Rather than proving 1 + 1 = 2 (I feel ridiculous), these lemmas should just happen later in mathlib, with stronger typeclasses. But these files are holding up the port, so its better to get this ported as is, and we can make it more sensible later... Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This file contains hidden or 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
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
3 participants
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.
#17646 move
zero_le_one_classtoalgebra.order.monoid.with_zero. This PR split things aboutzero_le_one_classinto two files.Also, all lemmas about numerics other than 0 and 1 require typeclass
add_monoid_with_onenow.Zulip