map from AddGroup to Group

Stream: mathlib4

[Noah G. Singer]

Is there a type for homomorphisms from an AddGroup to a Group (or more generally from an AddMonoid to a Monoid)? I spent a while poking around Mathlib this morning but didn't find anything. Thanks!

[Eric Wieser]

Maybe docs#AddChar ?

[Ruben Van de Velde]

Or something with docs#Multiplicative ?

[Noah G. Singer]

ahhh thanks! it would be nice if there was an AddChar.mk' that worked the same way as (Add)MonoidHom.mk' (so you only have to pass the hypothesis that the map is multiplicative). and maybe this should be linked from the monoidhom page? I can PR those?