Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/category): show categorical image in Module agrees with range#12605

Closed
kim-em wants to merge 4 commits intomasterfrom
semorrison/Module_images
Closed

[Merged by Bors] - feat(algebra/category): show categorical image in Module agrees with range#12605
kim-em wants to merge 4 commits intomasterfrom
semorrison/Module_images

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Mar 11, 2022

This just follows the existing code for the same fact in AddCommGroup.

This PR is preparing for a better API for homological calculations in Module R.


Open in Gitpod

@kim-em kim-em added the awaiting-CI The author would like to see what CI has to say before doing more work. label Mar 11, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 11, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Mar 12, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Mar 12, 2022
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

@kim-em kim-em added the awaiting-review The author would like community review of the PR label Mar 12, 2022
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Mar 14, 2022

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Mar 14, 2022
Co-authored-by: Johan Commelin <johan@commelin.net>
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Mar 15, 2022

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Mar 15, 2022
bors bot pushed a commit that referenced this pull request Mar 15, 2022
…range (#12605)

This just follows the existing code for the same fact in `AddCommGroup`.

This PR is preparing for a better API for homological calculations in `Module R`.





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Mar 15, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/category): show categorical image in Module agrees with range [Merged by Bors] - feat(algebra/category): show categorical image in Module agrees with range Mar 15, 2022
@bors bors bot closed this Mar 15, 2022
@bors bors bot deleted the semorrison/Module_images branch March 15, 2022 03:40
laurentbartholdi pushed a commit that referenced this pull request Mar 17, 2022
…range (#12605)

This just follows the existing code for the same fact in `AddCommGroup`.

This PR is preparing for a better API for homological calculations in `Module R`.





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants