# Actions by Subgroups #

These are just copies of the definitions about Submonoid starting from Submonoid.mulAction.

## Tags #

subgroup, subgroups

instance AddSubgroup.instAddAction {G : Type u_1} {α : Type u_2} [] [] {S : } :

Equations
instance Subgroup.instMulAction {G : Type u_1} {α : Type u_2} [] [] {S : } :
MulAction (S) α

The action by a subgroup is the action by the underlying group.

Equations
theorem AddSubgroup.vadd_def {G : Type u_1} {α : Type u_2} [] [] {S : } (g : S) (m : α) :
g +ᵥ m = g +ᵥ m
theorem Subgroup.smul_def {G : Type u_1} {α : Type u_2} [] [] {S : } (g : S) (m : α) :
g m = g m
@[simp]
theorem AddSubgroup.mk_vadd {G : Type u_1} {α : Type u_2} [] [] {S : } (g : G) (hg : g S) (a : α) :
{ val := g, property := hg } +ᵥ a = g +ᵥ a
@[simp]
theorem Subgroup.mk_smul {G : Type u_1} {α : Type u_2} [] [] {S : } (g : G) (hg : g S) (a : α) :
{ val := g, property := hg } a = g a
instance AddSubgroup.vaddCommClass_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [VAdd α β] [] (S : ) :
Equations
instance Subgroup.smulCommClass_left {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [SMul α β] [] (S : ) :
SMulCommClass (S) α β
Equations
instance AddSubgroup.vaddCommClass_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [VAdd α β] [] [] (S : ) :
Equations
instance Subgroup.smulCommClass_right {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [SMul α β] [] [] (S : ) :
SMulCommClass α (S) β
Equations

Note that this provides IsScalarTower S G G which is needed by smul_mul_assoc.

Equations

The action by a subgroup is the action by the underlying group.

Equations

The action by a subgroup is the action by the underlying group.

Equations
instance Subgroup.center.smulCommClass_left {G : Type u_1} [] :
SMulCommClass (()) G G

The center of a group acts commutatively on that group.

Equations
instance Subgroup.center.smulCommClass_right {G : Type u_1} [] :
SMulCommClass G (()) G

The center of a group acts commutatively on that group.

Equations