Stream: maths

Topic: sub_mul_action

Chris Hughes (Jun 01 2019 at 13:05):

Do we want this class, and should it be bundled?

class is_sub_mul_action (α : Type*) (β : Type*) [monoid α] [mul_action α β] (s : set β) : Prop :=
(smul_mem : ∀ (x : β) (r : α), x ∈ s → r • x ∈ s)


Is there any type class problems that this might cause. I know module caused problems, so I want to get it right. The application is that the conjugation action on subgroups of a group, is a sub-action of the action on sets. Similarly for the action on Sylow subgroups.

Kevin Buzzard (Jun 01 2019 at 14:56):

This is also sub-G-modules of a G-module

Last updated: May 14 2021 at 20:13 UTC