mathlib3

791d51c6 - feat(group_theory/group_action): a monoid action determines a monoid hom (#8253)

feat(group_theory/group_action): a monoid action determines a monoid hom (#8253) Defines the monoid hom `M -> category_theory.End X` (the latter is the monoid `X -> X`) corresponding to an action `mul_action M X` and vice versa. Split off from #7395