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/non_unital_alg_hom): define non_unital_alg_hom #7863
Conversation
The motivation is to be able to state the universal property for a magma algebra using bundled morphisms.
The plan is to split this PR in two since the other changes are deep and cause long build times.
This reverts commit 880e44b.
🎉 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! |
I missed this when I generalised from extending linear_map to extending distrib_mul_action_hom
Missed these in earlier work.
This all looks very uncontroversial. Maybe you should say something about planned usage of this structure in the module docstring? |
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.
bors d+
I think it would be worth adding a comment along the lines of TODO: add `non_unital_alg_equiv` when needed
in the module docstring. I don't think it's necessary to actually add it in this PR though.
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
The motivation is to be able to state the universal property for a magma algebra using bundled morphisms.
bors r- |
Canceled. |
The motivation is to be able to state the universal property for a magma algebra using bundled morphisms.
Pull request successfully merged into master. Build succeeded: |
The motivation is to be able to state the universal property for a magma algebra using bundled morphisms.
If we merge this, then I should be able to drop #6591 completely.
inverse
defs #7847