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] - chore: split CategoryTheory.MorphismProperty #12393
Conversation
Did you mean to mark this awaiting-review? If so, feel free to do so - if not, happy polishing :-) |
CI was broken earlier today, so that it did not mark it so then, but now it is. |
This seems good according to #12455 |
🚀 Pull request has been placed on the maintainer queue by erdOne. |
Thanks! bors merge |
The file `CategoryTheory.MorphismProperty` is split into five files `Basic`, `Composition`, `Limits`, `Concrete`, `IsInvertedBy`.
Pull request successfully merged into master. Build succeeded: |
The file `CategoryTheory.MorphismProperty` is split into five files `Basic`, `Composition`, `Limits`, `Concrete`, `IsInvertedBy`.
The file `CategoryTheory.MorphismProperty` is split into five files `Basic`, `Composition`, `Limits`, `Concrete`, `IsInvertedBy`.
The file
CategoryTheory.MorphismProperty
is split into five filesBasic
,Composition
,Limits
,Concrete
,IsInvertedBy
.