# mathlib3documentation

group_theory.subgroup.actions

# Actions by subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

These are just copies of the definitions about submonoid starting from submonoid.mul_action.

## Tags #

subgroup, subgroups

@[protected, instance]
α

Equations
@[protected, instance]
def subgroup.mul_action {G : Type u_1} [group G] {α : Type u_2} [ α] (S : subgroup G) :
α

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

Equations
theorem subgroup.smul_def {G : Type u_1} [group G] {α : Type u_2} [ α] {S : subgroup G} (g : S) (m : α) :
g m = g m
theorem add_subgroup.vadd_def {G : Type u_1} [add_group G] {α : Type u_2} [ α] {S : add_subgroup G} (g : S) (m : α) :
g +ᵥ m = g +ᵥ m
@[protected, instance]
def subgroup.smul_comm_class_left {G : Type u_1} [group G] {α : Type u_2} {β : Type u_3} [ β] [ β] [ β] (S : subgroup G) :
β
@[protected, instance]
def add_subgroup.vadd_comm_class_left {G : Type u_1} [add_group G] {α : Type u_2} {β : Type u_3} [ β] [ β] [ β] (S : add_subgroup G) :
β
@[protected, instance]
def subgroup.smul_comm_class_right {G : Type u_1} [group G] {α : Type u_2} {β : Type u_3} [ β] [ β] [ β] (S : subgroup G) :
β
@[protected, instance]
def add_subgroup.vadd_comm_class_right {G : Type u_1} [add_group G] {α : Type u_2} {β : Type u_3} [ β] [ β] [ β] (S : add_subgroup G) :
β
@[protected, instance]
def subgroup.is_scalar_tower {G : Type u_1} [group G] {α : Type u_2} {β : Type u_3} [ β] [ α] [ β] [ β] (S : subgroup G) :
β

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

@[protected, instance]
def subgroup.has_faithful_smul {G : Type u_1} [group G] {α : Type u_2} [ α] [ α] (S : subgroup G) :
@[protected, instance]
def subgroup.distrib_mul_action {G : Type u_1} [group G] {α : Type u_2} [add_monoid α] [ α] (S : subgroup G) :

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

Equations
@[protected, instance]
def subgroup.mul_distrib_mul_action {G : Type u_1} [group G] {α : Type u_2} [monoid α] (S : subgroup G) :

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

Equations
@[protected, instance]

The center of a group acts commutatively on that group.

@[protected, instance]

The center of a group acts commutatively on that group.