mathlib3

c10efa66 - refactor(algebra/hom/group): generalize basic API of `monoid_hom` to `monoid_hom_class` (#14997)

refactor(algebra/hom/group): generalize basic API of `monoid_hom` to `monoid_hom_class` (#14997) This PR generalizes part of the basic API of monoid homs to monoid_hom_class. This notably includes things like monoid_hom.mker, submonoid.map and submonoid.comap. I left the namespaces unchanged, for example `monoid_hom.mker` remains the same even though it is now defined for any `monoid_hom_class` morphism; this way dot notation still (mostly) works for actual monoid homs.