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