hom from mul monoid to add monoid

Stream: Is there code for X?

[FR]

Is there any way to write a homomorphism from a multiplicative monoid to an additive monoid?

[Riccardo Brasca]

You can use docs#multiplicative to turn an additive monoid into a multiplicative one, and then use the usual →* (or the other way if you prefer, using docs#additive)

[FR]

Looks great! I'll try it, thanks.

[Kevin Buzzard]

It doesn't look great. It works but that's about it. I do wonder whether this approach will scale. We take the cohomology of multiplicative objects and get additive objects quite a lot so this issue is coming our way.