Zulip Chat Archive

Stream: maths

Topic: multiplication is an add_monoid_hom


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

If RR 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: Dec 20 2023 at 11:08 UTC