mathlib3

3c7fd80d - Define `monoid_with_zero_hom_class` and its ancestors