Commit 2020-04-02 11:19 3c27d284
View on Github →feat(algebra/pi_instances): bundled homs for apply and single (#2186) feat(algebra/pi_instances): bundled homs for apply and single (#2186) This adds some bundled monoid homomorphisms, in particular
def monoid_hom.apply (i : I) : (Π i, f i) →* f i := ...
and
def add_monoid_hom.single (i : I) : f i →+ Π i, f i :=
and supporting lemmas.