Skip to content

[Merged by Bors] - feat: basic API for the right homology of short complexes#5250

Closed
joelriou wants to merge 2 commits intomasterfrom
shortcomplex_righthomology
Closed

[Merged by Bors] - feat: basic API for the right homology of short complexes#5250
joelriou wants to merge 2 commits intomasterfrom
shortcomplex_righthomology

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jun 19, 2023

This PR introduces the basic API for the right homology of short complexes.


In the next PR, we shall see that left and right homology are dual notions.

Open in Gitpod

@joelriou joelriou added awaiting-review and removed WIP Work in progress labels Jun 19, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jun 21, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 21, 2023
bors bot pushed a commit that referenced this pull request Jun 21, 2023
This PR introduces the basic API for the right homology of short complexes.
@bors
Copy link
Copy Markdown

bors bot commented Jun 21, 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: basic API for the right homology of short complexes [Merged by Bors] - feat: basic API for the right homology of short complexes Jun 21, 2023
@bors bors bot closed this Jun 21, 2023
@bors bors bot deleted the shortcomplex_righthomology branch June 21, 2023 02:40
alexkeizer pushed a commit that referenced this pull request Jun 22, 2023
This PR introduces the basic API for the right homology of short complexes.
kim-em pushed a commit that referenced this pull request Jun 23, 2023
This PR introduces the basic API for the right homology of short complexes.
kim-em pushed a commit that referenced this pull request Jun 23, 2023
This PR introduces the basic API for the right homology of short complexes.
kim-em pushed a commit that referenced this pull request Jun 25, 2023
This PR introduces the basic API for the right homology of short complexes.
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.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants