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