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

[Merged by Bors] - chore(linear_algebra/tensor_product): Actually relax the requirements for add_comm_group #5315

Closed

Conversation

eric-wieser
Copy link
Member

A previous commit (#5305) changed the definition to not need these, but forgot to actually change these.


… for add_comm_group

A previous commit changed the definition to not need these, but forgot to actually change these.
@eric-wieser eric-wieser added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Dec 11, 2020
Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch!
bors r+

@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 Dec 11, 2020
bors bot pushed a commit that referenced this pull request Dec 11, 2020
… for add_comm_group (#5315)

A previous commit (#5305) changed the definition to not need these, but forgot to actually change these.
@bors
Copy link

bors bot commented Dec 11, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(linear_algebra/tensor_product): Actually relax the requirements for add_comm_group [Merged by Bors] - chore(linear_algebra/tensor_product): Actually relax the requirements for add_comm_group Dec 11, 2020
@bors bors bot closed this Dec 11, 2020
@bors bors bot deleted the eric-wieser/actually-relax-tensor-semiring branch December 11, 2020 19:45
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
easy < 20s of review time. See the lifecycle page for guidelines. 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
Development

Successfully merging this pull request may close these issues.

2 participants