Kevin Buzzard (Apr 08 2020 at 17:24):
If 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
Johan Commelin (Apr 08 2020 at 17:38):
Well, it's not
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
Last updated: May 12 2021 at 07:17 UTC