-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/star): star monoids, rings and algebras #4886
Conversation
271c1f0
to
26117cf
Compare
26117cf
to
ea651b4
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
Once this goes in, I'll add some instances for |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Thanks @bryangingechen, updated |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
Please fix the merge conflict, and merge afterwards.
bors d+
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This takes the parts of #4685 and #4686 which do not concern themselves with
ordering
, thus removing the dependency on a stale PR. I don't expect this to cause any difficult merge conflicts if this goes in before the other two,as the lines have been copied without modification.Changes made on top of Scott's work:
_equiv
structures