pi): add pi.monoid_hom (#17757)

Commit

3 years ago

feat(algebra/group/pi): add pi.monoid_hom (#17757) Add the `monoid` version of `pi.ring_hom`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

xroblot

Parents