Def distrib_mul_action.comp_hom

chore(algebra/*): make non-instance typeclasses reducible. (#8322) …

refactor(algebra/add_torsor): use `to_additive` for `add_action` (#6914)

chore(group_theory/group_action/defs): combine duplicated `comp_hom` and rename derivative definitions (#6942) …