Commit 2020-11-17 12:21 86b09715

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