mathlib

3c27d284 - feat(algebra/pi_instances): bundled homs for apply and single (#2186)

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.