## Stream: maths

### Topic: multiplication is an add_monoid_hom

#### Kevin Buzzard (Apr 08 2020 at 17:24):

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 (Apr 08 2020 at 17:26):

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

#### Kevin Buzzard (Apr 08 2020 at 17:34):

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 (Apr 08 2020 at 17:38):

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

#### Johan Commelin (Apr 08 2020 at 17:38):

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

#### Kevin Buzzard (Apr 08 2020 at 17:45):

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

#### Yury G. Kudryashov (Apr 08 2020 at 17:53):

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

Last updated: May 12 2021 at 07:17 UTC