sub_mul_action

Stream: maths

[Chris Hughes]

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]

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