feat(group/hom_instances): add composition operators (#7407)
This adds the analogous definitions to those we have for `linear_map`, namely:
* `monoid_hom.comp_hom'` (c.f. `linear_map.lcomp`, `l` = `linear`)
* `monoid_hom.compl₂` (c.f. `linear_map.compl₂`, `l` = `left`)
* `monoid_hom.compr₂` (c.f. `linear_map.compr₂`, `r` = `right`)
We already have `monoid_hom.comp_hom` (c.f. `linear_map.llcomp`, `ll` = `linear linear`)
It also adds an `ext_iff₂` lemma, which is occasionally useful (but not present for any other time at the moment).
The order of definitions in the file has been shuffled slightly to permit addition of a subheading to group things in doc-gen
