THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
A monoid homomorphism between groups with zeros sending
We define the inverse as a
monoid_with_zero_hom by extending the inverse map by zero
Inversion on a commutative group with zero, considered as a monoid with zero homomorphism.