pi.monoid_hom

Stream: Is there code for X?

[Xavier Roblot]

There is docs#pi.ring_hom to construct a ring homomorphism f : R →+* Π i, S i from a family of ring homomorphisms f i : R →+* S i, but I could not find the equivalent for monoid_hom. Does it exist somewhere?

[Eric Wieser]

docs#linear_map.pi exists too, with a different naming convention

[Riccardo Brasca]

Wow, it's really surprising we don't have it!

[Xavier Roblot]

#17757
(I am not sure I used to_additive correctly though).