Skip to content

[Merged by Bors] - feat: the type of cocycles in the complex of morphisms between cochain complexes#7201

Closed
joelriou wants to merge 3 commits intomasterfrom
homcomplex2
Closed

[Merged by Bors] - feat: the type of cocycles in the complex of morphisms between cochain complexes#7201
joelriou wants to merge 3 commits intomasterfrom
homcomplex2

Conversation

@joelriou
Copy link
Copy Markdown
Contributor


Open in Gitpod

joelriou and others added 2 commits September 15, 2023 22:16
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou joelriou changed the title feat: the type of cocycles in the complex of morphisms between cochan complexes feat: the type of cocycles in the complex of morphisms between cochain complexes Sep 15, 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 19, 2023
bors bot pushed a commit that referenced this pull request Sep 19, 2023
@bors
Copy link
Copy Markdown

bors bot commented Sep 19, 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: the type of cocycles in the complex of morphisms between cochain complexes [Merged by Bors] - feat: the type of cocycles in the complex of morphisms between cochain complexes Sep 19, 2023
@bors bors bot closed this Sep 19, 2023
@bors bors bot deleted the homcomplex2 branch September 19, 2023 08:20
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
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.

2 participants