# Documentation

Mathlib.GroupTheory.Subgroup.Actions

# Actions by Subgroups #

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

## Tags #

subgroup, subgroups

The additive action by an add_subgroup is the action by the underlying AddGroup.

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

theorem AddSubgroup.vadd_def {G : Type u_1} [] {α : Type u_2} [] {S : } (g : { x // x S }) (m : α) :
g +ᵥ m = g +ᵥ m
theorem Subgroup.smul_def {G : Type u_1} [] {α : Type u_2} [] {S : } (g : { x // x S }) (m : α) :
g m = g m
theorem AddSubgroup.vaddCommClass_left.proof_1 {G : Type u_1} [] {α : Type u_2} {β : Type u_3} [] [VAdd α β] [] (S : ) :
instance AddSubgroup.vaddCommClass_left {G : Type u_1} [] {α : Type u_2} {β : Type u_3} [] [VAdd α β] [] (S : ) :
VAddCommClass { x // x S } α β
instance Subgroup.smulCommClass_left {G : Type u_1} [] {α : Type u_2} {β : Type u_3} [] [SMul α β] [] (S : ) :
SMulCommClass { x // x S } α β
instance AddSubgroup.vaddCommClass_right {G : Type u_1} [] {α : Type u_2} {β : Type u_3} [VAdd α β] [] [] (S : ) :
VAddCommClass α { x // x S } β
theorem AddSubgroup.vaddCommClass_right.proof_1 {G : Type u_1} [] {α : Type u_2} {β : Type u_3} [VAdd α β] [] [] (S : ) :
instance Subgroup.smulCommClass_right {G : Type u_1} [] {α : Type u_2} {β : Type u_3} [SMul α β] [] [] (S : ) :
SMulCommClass α { x // x S } β

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

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

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

instance Subgroup.center.smulCommClass_left {G : Type u_1} [] :
SMulCommClass { x // } G G

The center of a group acts commutatively on that group.

instance Subgroup.center.smulCommClass_right {G : Type u_1} [] :
SMulCommClass G { x // } G

The center of a group acts commutatively on that group.