mathlib

c8243a6a - feat(group_theory/submonoid/basic): add `monoid_hom.of_mclosure_eq_top_left` (#16809)

feat(group_theory/submonoid/basic): add `monoid_hom.of_mclosure_eq_top_left` (#16809) * rename `monoid_hom.of_mdense` to `monoid_hom.of_mclosure_eq_top_right`; * add `monoid_hom.of_mclosure_eq_top_left`.