[Merged by Bors] - feat: port CategoryTheory.Abelian.Basic#2769
Closed
mattrobball wants to merge 19 commits intomasterfrom
Closed
[Merged by Bors] - feat: port CategoryTheory.Abelian.Basic#2769mattrobball wants to merge 19 commits intomasterfrom
mattrobball wants to merge 19 commits intomasterfrom
Conversation
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Now we have `PreservesFiniteProducts` and `PreservesFiniteCoproducts` as separate classes
…tsAndEqualizers' into port/CategoryTheory.Abelian.Basic
Contributor
|
This PR/issue depends on: |
c616fe7 to
d592edf
Compare
Contributor
Author
|
The problem with |
Contributor
|
Bumped to master in case Gabriel's changes in nightly-2023-03-17 help. |
Contributor
Author
|
Thanks. When I bumped on my own machine, it didn't but 🤞 |
Contributor
|
Here's the snippet that shows that this really is leanprover/lean4#2055 |
Contributor
|
Okay, we can just remove the troublesome instance. I've made a mathlib3 PR that verifies that removing the instance doesn't cause trouble downstream. I've left a porting note (and added one on the mathlib3 side), so hopefully when leanprover/lean4#2055 is resolved we will remember to clean this up again. |
Contributor
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Apr 5, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
MonadMaverick
pushed a commit
that referenced
this pull request
Apr 9, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
MonadMaverick
pushed a commit
that referenced
this pull request
Apr 9, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot
pushed a commit
to leanprover-community/mathlib3
that referenced
this pull request
Apr 28, 2023
…e_biproducts instance (#18740) This backports a proposed removal of the `abelian.has_finite_biproducts` global instance, instead enabling it locally in the files that need it. The reason for removing it is that it triggers the ~~dreaded~~ leanprover/lean4#2055 during the simpNF linter in leanprover-community/mathlib4#2769, the mathlib4 port of `category_theory.abelian.basic`. This backport verifies that we won't run into further problems downstream if we (hopefully temporarily) remove these instances in mathlib4. 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 join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Uh oh!
There was an error while loading. Please reload this page.