Skip to content

[Merged by Bors] - feat(Condensed): light condensed modules#13501

Closed
dagurtomas wants to merge 1 commit intomasterfrom
dagur/LightCondMod
Closed

[Merged by Bors] - feat(Condensed): light condensed modules#13501
dagurtomas wants to merge 1 commit intomasterfrom
dagur/LightCondMod

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor


Open in Gitpod

@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory t-condensed Condensed mathematics labels Jun 4, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 4, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 5, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 5, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Condensed): light condensed modules [Merged by Bors] - feat(Condensed): light condensed modules Jun 5, 2024
@mathlib-bors mathlib-bors bot closed this Jun 5, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/LightCondMod branch June 5, 2024 20:11
mathlib-bors bot pushed a commit that referenced this pull request Jun 7, 2024
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 t-condensed Condensed mathematics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants