Skip to content

[Merged by Bors] - feat: first definitions in the API for the homology of short complexes#6443

Closed
joelriou wants to merge 50 commits intomasterfrom
shortcomplex_homology2
Closed

[Merged by Bors] - feat: first definitions in the API for the homology of short complexes#6443
joelriou wants to merge 50 commits intomasterfrom
shortcomplex_homology2

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Aug 8, 2023

In this PR, some basic constructions for left and right homology of short complexes are combined.


Open in Gitpod

joelriou and others added 30 commits July 2, 2023 21:53
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Aug 11, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 13, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 20, 2023
@ghost
Copy link
Copy Markdown

ghost commented Aug 20, 2023

@TwoFX TwoFX added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Aug 28, 2023
@joelriou joelriou added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Aug 29, 2023
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.

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 4, 2023
bors bot pushed a commit that referenced this pull request Sep 4, 2023
#6443)

In this PR, some basic constructions for left and right homology of short complexes are combined.



Co-authored-by: Joël Riou <[email protected]>
@bors
Copy link
Copy Markdown

bors bot commented Sep 4, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: first definitions in the API for the homology of short complexes [Merged by Bors] - feat: first definitions in the API for the homology of short complexes Sep 4, 2023
@bors bors bot closed this Sep 4, 2023
@bors bors bot deleted the shortcomplex_homology2 branch September 4, 2023 15:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants