mathlib3

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

feat(group_theory/group_action): Extract a smaller typeclass out of `mul_semiring_action` (#8918) This new typeclass, `mul_distrib_mul_action`, is satisfied by conjugation actions. This PR provides instances for: * `mul_aut` * `prod` of two types with a `mul_distrib_mul_action` * `pi` of types with a `mul_distrib_mul_action` * `units` of types with a `mul_distrib_mul_action` * `ulift` of types with a `mul_distrib_mul_action` * `opposite` of types with a `mul_distrib_mul_action` * `sub(monoid|group|semiring|ring)`s of types with a `mul_distrib_mul_action` * anything already satisfying a `mul_semiring_action`