Commit 2021-07-22 12:14 791d51c6
View on Github →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