Theorem smul_mul'

feat(group_theory/group_action): Extract a smaller typeclass out of `mul_semiring_action` (#8918) …

feat(algebra/group_ring_action) define group actions on rings (#2566) …