notation for group action

Stream: kbb

[Johan Commelin]

I think we should just group actions an instance of has_smul. What do others think?

[Mario Carneiro]

it probably won't cause problems

[Johan Commelin]

And then we get group_module G A with an instance to module (group_ring G) A and we will have to versions of has_smul :scream:

[Johan Commelin]

Ooo, I guess it just means we will always have to explicitly write the coercion G → (group_ring G) to distinguish which action we mean.