mathlib3

1efa3673 - feat(group_action/defs): add missing comp_hom smul instances (#8707)

feat(group_action/defs): add missing comp_hom smul instances (#8707) This adds missing `smul_comm_class` and `is_scalar_tower` instances about the `comp_hom` definitions. To resolve unification issues in finding these instances caused by the reducibility of the `comp_hom` defs, this introduces a semireducible def `has_scalar.comp.smul`.