Commit 2021-09-08 14:00 7a2ccb6a

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