hom): Notation for `monoid_with_zero_hom` (#11632)

Commit

3 years ago

feat(algebra/group/hom): Notation for `monoid_with_zero_hom` (#11632) Introduce notation `→*₀` for `monoid_with_zero_hom` and use it everywhere.

Author

YaelDillies

Parents