Mathlib v3 is deprecated. Go to Mathlib v4

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 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

Estimated changes