There's MonoidHom and AddMonoidHom but I need something else

Stream: Is there code for X?

[ohhaimark]

I want to have a hom instance for a map from angles to rotation matrices, but those go from an AddMonoid to a Monoid. Am I missing something?

[Riccardo Brasca]

You can consider a MonoidHom from Multiplicative angles. See docs#Multiplicative.

[Aaron Liu]

You could consider going from Circle

[Kenny Lau]

clearly nobody knows about Orientation.rotation (and yeah it's a bit bad)

[Kenny Lau]

maybe it's time for an AddMulHom

[Kenny Lau]

we can make its symbol +→*

[Aaron Liu]

it's an exponential map

[Aaron Liu]

and if you also add in logarithmic maps you end up with six new ways to compose them together and fourteen new associativity lemmas

[Kenny Lau]

sounds fun

[Yury G. Kudryashov]

We already have docs#AddChar