mathlib

07c57b56 - feat(group_theory): Add `monoid_hom.mker` and generalise the codomain for `monoid_hom.ker` (#8532)

feat(group_theory): Add `monoid_hom.mker` and generalise the codomain for `monoid_hom.ker` (#8532) Add `monoid_hom.mker` for `f : M ->* N`, where `M` and `N` are `mul_one_class`es, and `monoid_hom.ker` is now defined for `f : G ->* H`, where `H` is a `mul_one_class`