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

[Merged by Bors] - feat(algebra/category/Module): free module functor is lax monoidal #6906

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(algebra/category/Module): free module functor is lax monoidal #6906

wants to merge 7 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Mar 27, 2021 •
edited by github-actions bot
Loading

@github-actions github-actions bot 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 27, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 2, 2021
@github-actions github-actions bot removed merge-conflict Please `git merge origin/master` then a bot will remove this label. blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Apr 5, 2021
@github-actions
Copy link

github-actions bot commented Apr 6, 2021

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 6, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 6, 2021
@semorrison semorrison added the awaiting-review The author would like community review of the PR label Apr 6, 2021
jcommelin
jcommelin approved these changes Apr 7, 2021
View reviewed changes
Copy link
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

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 7, 2021
bors bot pushed a commit that referenced this pull request Apr 7, 2021
@semorrison
feat(algebra/category/Module): free module functor is lax monoidal (#…
919b4e3 
…6906)




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

bors bot commented Apr 7, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/category/Module): free module functor is lax monoidal [Merged by Bors] - feat(algebra/category/Module): free module functor is lax monoidal Apr 7, 2021
@bors bors bot closed this Apr 7, 2021
@bors bors bot deleted the free_module_monoidal branch April 7, 2021 19:05
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@semorrison @jcommelin