-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: port CategoryTheory.Idempotents.KaroubiKaroubi #3298
Conversation
joelriou
commented
Apr 6, 2023
•
edited by github-actions
bot
edited by github-actions
bot
- depends on: [Merged by Bors] - feat: port CategoryTheory.Idempotents.Basic #3290
- depends on: [Merged by Bors] - feat: port CategoryTheory.Idempotents.Karoubi #3291
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
…ryTheory.Idempotents.Karoubi
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
…Karoubi' into port/CategoryTheory.Idempotents.KaroubiKaroubi
…tents.KaroubiKaroubi
This PR/issue depends on: |
variable (C : Type _) [Category C] | ||
|
||
-- porting note: added to ease automation | ||
@[simp] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this also be reassoc
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks. Yes, indeed it should. I have just added it.
bors merge |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>