Commit 2021-09-16 13:26 ca383574
View on Github →feat(group_theory/group_action): add distrib_mul_action.to_add_aut and mul_distrib_mul_action.to_mul_aut (#9224)
These can be used to golf the existing mul_aut_arrow.
This also moves some definitions out of algebra/group_ring_action.lean into a more appropriate file.