## Stream: maths

### Topic: groups acting on sets

#### Kevin Buzzard (Jan 31 2019 at 15:42):

Did we ever get groups acting on sets? [or even monoids acting on sets?]. The reason I ask is that I just tried to define groups acting on abelian groups and I realised I can't use * because the action is G -> M -> M. Has a decision been made about notation for groups acting on anything other than themselves?

#### Johan Commelin (Jan 31 2019 at 15:45):

Yes, these are in mathlib, and you want to use smul, I think.

#### Johan Commelin (Jan 31 2019 at 15:45):

\bullet

#### Kevin Buzzard (Jan 31 2019 at 15:55):

Apparently it's \bu now. And I have to import algebra.module to get the notation :-) It should be some far more primitive thing. Is the fact that the notation is defined in algebra.module evidence that we don't have groups acting on sets yet?

#### Kenny Lau (Jan 31 2019 at 16:20):

Did we ever get groups acting on sets? [or even monoids acting on sets?]. The reason I ask is that I just tried to define groups acting on abelian groups and I realised I can't use * because the action is G -> M -> M. Has a decision been made about notation for groups acting on anything other than themselves?

is_group_action

#### Kenny Lau (Jan 31 2019 at 16:20):

also when I did it myself I used \ci

Last updated: May 10 2021 at 08:14 UTC