Zulip Chat Archive

Stream: Is there code for X?

Topic: Right multiplication in a monoid

Noam Atar (Jul 24 2023 at 20:52):

Hey, is there code for the fact that right multiplication in a monoid is a (left) SMul-homomorphism?

Eric Wieser (Jul 24 2023 at 21:00):

docs#DistribMulAction.toLinearMap, maybe?

Eric Wieser (Jul 24 2023 at 21:02):

SMul-homomorphisms are very undeveloped, so I doubt you'll find the result for docs#MulActionHom

Eric Wieser (Jul 24 2023 at 21:02):

Oh, nevermind: docs#SMulCommClass.toMulActionHom !

Noam Atar (Jul 24 2023 at 21:10):

And a monoid is automatically a SMulCommClass?

Eric Wieser (Jul 24 2023 at 21:35):

Yes

Eric Wieser (Jul 24 2023 at 21:36):

That is, we have SMulCommClass M Mᵐᵒᵖ M already somewhere

Noam Atar (Jul 25 2023 at 05:14):

Cool, thanks!

Noam Atar (Jul 25 2023 at 17:12):

Eric Wieser said:

That is, we have SMulCommClass M Mᵐᵒᵖ M already somewhere

Are you sure of this? I searched the codebase for M Mᵐᵒᵖ M and didn't find anything...

Kevin Buzzard (Jul 25 2023 at 17:14):

You'll have more luck searching for SMulCommClass α αᵐᵒᵖ α... (docs#Semigroup.opposite_smulCommClass')

Adam Topaz (Jul 25 2023 at 17:17):

you can find such things as follows:

import Mathlib

variable (M : Type _) [Monoid M]
#synth (SMulCommClass M Mᵐᵒᵖ M)

Noam Atar (Jul 25 2023 at 17:21):

Cool! I'll try that next time!

Last updated: Dec 20 2023 at 11:08 UTC