Zulip Chat Archive

Stream: kbb

Topic: notation for group action


view this post on Zulip Johan Commelin (Sep 14 2018 at 05:01):

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

view this post on Zulip Mario Carneiro (Sep 14 2018 at 05:03):

it probably won't cause problems

view this post on Zulip Johan Commelin (Sep 14 2018 at 05:04):

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:

view this post on Zulip Johan Commelin (Sep 14 2018 at 05:33):

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.


Last updated: May 18 2021 at 11:11 UTC