mathlib3
2726e238 - feat(algebra.group.hom_instances): Define left and right multiplication operators (#11843)

Commit
3 years ago
feat(algebra.group.hom_instances): Define left and right multiplication 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>
Author
Parents
Loading