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.group.hom_instances): Define left and right multiplication operators #11843

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat(algebra.group.hom_instances): Define left and right multiplication operators #11843

wants to merge 2 commits into from

Conversation

mans0954
Copy link
Collaborator

@mans0954 mans0954 commented Feb 4, 2022

Defines left and right multiplication operators on non unital, non associative semirings.

Suggested by @ocfnash for #11073

Open in Gitpod

@mans0954 mans0954 added the awaiting-review The author would like community review of the PR label Feb 4, 2022
@mans0954 mans0954 mentioned this pull request Feb 4, 2022
Closed
4 tasks
ocfnash
ocfnash approved these changes Feb 9, 2022
View reviewed changes
Copy link
Collaborator

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

bors d+

src/algebra/group/hom_instances.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Feb 9, 2022

✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Feb 9, 2022
@mans0954 @ocfnash
Update src/algebra/group/hom_instances.lean
279326a 
Co-authored-by: Oliver Nash <github@olivernash.org>
@mans0954
Copy link
Collaborator Author

mans0954 commented Feb 9, 2022

bors r+

bors bot pushed a commit that referenced this pull request Feb 9, 2022
@mans0954
feat(algebra.group.hom_instances): Define left and right multiplicati…
2726e23 
…on operators (#11843)

Defines left and right multiplication operators on non unital, non associative semirings.

Suggested by @ocfnash for #11073



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 9, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra.group.hom_instances): Define left and right multiplication operators [Merged by Bors] - feat(algebra.group.hom_instances): Define left and right multiplication operators Feb 9, 2022
@bors bors bot closed this Feb 9, 2022
@bors bors bot deleted the add_monoid_end_mult_op branch February 9, 2022 20:38
@mans0954 mans0954 mentioned this pull request Feb 9, 2022
Closed
bors bot pushed a commit that referenced this pull request Feb 9, 2022
@mans0954
doc(algebra/group/hom_instances): Fix spellings (#11943)
4691159 
Fixes spelling mistakes introduced by #11843
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@ocfnash ocfnash ocfnash approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@mans0954 @ocfnash @leanprover-community-bot-assistant