multiplication is an add_monoid_hom

Stream: maths

[Kevin Buzzard]

If $R$ is a semiring, then left and right multiplication by r : R are add_monoid_homs. Do we have this definition in mathlib?

[Johan Commelin]

I think we have smul as a linear map on modules... That would be defeq to your left multiplication.

[Kevin Buzzard]

The reason I asked is Scott's comment here; I can't use modules in data.list.basic I suspect. (to be honest, I was surprised I could use add_monoid_homs!)

[Yury G. Kudryashov]

list.basic depends on data.nat.basic which depends on algebra.ordered_ring.

[Johan Commelin]

Well, it's not data.list.defs...

[Kevin Buzzard]

I can find the unbundled version but not the bundled version.

[Yury G. Kudryashov]

I think you should add it to algebra/group/hom