mathlib

ca383574 - feat(group_theory/group_action): add `distrib_mul_action.to_add_aut` and `mul_distrib_mul_action.to_mul_aut` (#9224)

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.