Topic: notation for group action
Johan Commelin (Sep 14 2018 at 05:01):
I think we should just group actions an instance of
has_smul. What do others think?
Mario Carneiro (Sep 14 2018 at 05:03):
it probably won't cause problems
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
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