mathlib

242d6875 - feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526)

feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526) The discussion and poll related to this new notation can be found in this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ring_hom.20notation.20and.20friends/near/279313301)