Commit 2021-04-30 05:44 39a1cf0b
View on Github →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 havemonoid_hom.comp_hom(c.f.linear_map.llcomp,ll=linear linear) It also adds anext_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