# Commit 2020-11-17 12:21 86b09715

View on Github →feat(algebra/group_with_zero): Bundled `monoid_with_zero_hom`

(#4995)
This adds, without notation, `monoid_with_zero_hom`

as a variant of `A →* B`

that also satisfies `f 0 = 0`

.
As part of this, this change:

- Splits up
`group_with_zero`

into multiple files, so that the definitions can be used in the bundled homs before any of the lemmas start pulling in dependencies - Adds
`monoid_with_zero_hom`

as a base class of`ring_hom`

- Changes some
`monoid_hom`

objects into`monoid_with_zero_hom`

objects. - Moves some lemmas about
`valuation`

into`monoid_hom`

, since they apply more generally - Add automatic coercions between
`monoid_with_zero_hom`

and`monoid_hom`