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 : } :

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

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 : α) :
g, hg +ᵥ a = g +ᵥ a
@[simp]
theorem Subgroup.mk_smul {G : Type u_1} {α : Type u_2} [] [] {S : } (g : G) (hg : g S) (a : α) :
g, 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
• =
instance Subgroup.instIsScalarTowerSubtypeMem {G : Type u_1} {α : Type u_2} {β : Type u_3} [] [SMul α β] [] [] [] (S : ) :
IsScalarTower (S) α β

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

Equations
• =
instance Subgroup.instFaithfulSMulSubtypeMem {G : Type u_1} {α : Type u_2} [] [] [] (S : ) :
FaithfulSMul (S) α
Equations
• =
instance Subgroup.instDistribMulActionSubtypeMem {G : Type u_1} {α : Type u_2} [] [] [] (S : ) :

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

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

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
• =