mathlib3

4f81077a - feat(group_theory/subgroup/basic): generalize `monoid_hom.eq_locus` (#17748)

feat(group_theory/subgroup/basic): generalize `monoid_hom.eq_locus` (#17748) Only assume that the codomain is a `monoid`. Also rename `monoid_hom.gclosure_preimage_le` to `monoid_hom.closure_preimage_le`.