mathlib3

de7dbbbd - feat(algebra/group): composition of monoid homs as "bilinear" monoid hom (#5202)