Actions by Submonoids

These instances transfer the action by an element m : M of a monoid M written as m • a onto the action by an element s : S of a submonoid S : Submonoid M such that s • a = (s : M) • a.

These instances work particularly well in conjunction with Monoid.toMulAction, enabling s • m as an alias for ↑s * m.

@[instance_reducible, instance 100]

instance Submonoid.instSMulSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [SMul M' α] : SMul (↥s) α

Equations

• Submonoid.instSMulSubtypeMem s = { smul := fun (m : ↥s) (a : α) => ↑m • a }

@[instance_reducible, instance 100]

instance AddSubmonoid.instVAddSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [VAdd M' α] : VAdd (↥s) α

Equations

• AddSubmonoid.instVAddSubtypeMem s = { vadd := fun (m : ↥s) (a : α) => ↑m +ᵥ a }

@[instance 100]

instance Submonoid.instIsLeftCancelSMulSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [SMul M' α] [IsLeftCancelSMul M' α] : IsLeftCancelSMul (↥s) α

@[instance 100]

instance AddSubmonoid.instIsLeftCancelVAddSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [VAdd M' α] [IsLeftCancelVAdd M' α] : IsLeftCancelVAdd (↥s) α

@[instance 100]

instance Submonoid.instIsCancelSMulSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [SMul M' α] [IsCancelSMul M' α] : IsCancelSMul (↥s) α

@[instance 100]

instance AddSubmonoid.instIsCancelVAddSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [VAdd M' α] [IsCancelVAdd M' α] : IsCancelVAdd (↥s) α

@[instance 100]

instance Submonoid.instSMulCommClassSubtypeMem {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [SetLike S' M'] (s : S') [SMul M' β] [SMul α β] [SMulCommClass M' α β] : SMulCommClass (↥s) α β

@[instance 100]

instance AddSubmonoid.instVAddCommClassSubtypeMem {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [SetLike S' M'] (s : S') [VAdd M' β] [VAdd α β] [VAddCommClass M' α β] : VAddCommClass (↥s) α β

@[instance 100]

instance Submonoid.instSMulCommClassSubtypeMem_1 {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [SetLike S' M'] (s : S') [SMul α β] [SMul M' β] [SMulCommClass α M' β] : SMulCommClass α (↥s) β

@[instance 100]

instance AddSubmonoid.instVAddCommClassSubtypeMem_1 {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [SetLike S' M'] (s : S') [VAdd α β] [VAdd M' β] [VAddCommClass α M' β] : VAddCommClass α (↥s) β

@[instance 100]

instance Submonoid.instIsScalarTowerSubtypeMem {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [SetLike S' M'] (s : S') [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] : IsScalarTower (↥s) α β

@[instance 100]

instance AddSubmonoid.instVAddAssocClassSubtypeMem {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [SetLike S' M'] (s : S') [VAdd α β] [VAdd M' α] [VAdd M' β] [VAddAssocClass M' α β] : VAddAssocClass (↥s) α β

@[instance_reducible, instance 100]

instance Submonoid.instMulActionSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [Monoid M'] [SubmonoidClass S' M'] [MulAction M' α] : MulAction (↥s) α

Equations

• Submonoid.instMulActionSubtypeMem s = { toSMul := Submonoid.instSMulSubtypeMem s, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible, instance 100]

instance AddSubmonoid.instAddActionSubtypeMem {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [SetLike S' M'] (s : S') [AddMonoid M'] [AddSubmonoidClass S' M'] [AddAction M' α] : AddAction (↥s) α

Equations

• AddSubmonoid.instAddActionSubtypeMem s = { toVAdd := AddSubmonoid.instVAddSubtypeMem s, add_vadd := ⋯, zero_vadd := ⋯ }

@[instance_reducible]

instance Submonoid.smul {M' : Type u_1} {α : Type u_2} [MulOneClass M'] [SMul M' α] (S : Submonoid M') : SMul (↥S) α

Equations

• S.smul = inferInstance

@[instance_reducible]

instance AddSubmonoid.vadd {M' : Type u_1} {α : Type u_2} [AddZeroClass M'] [VAdd M' α] (S : AddSubmonoid M') : VAdd (↥S) α

Equations

• S.vadd = inferInstance

instance Submonoid.smulCommClass_left {M' : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass M'] [SMul M' β] [SMul α β] [SMulCommClass M' α β] (S : Submonoid M') : SMulCommClass (↥S) α β

instance AddSubmonoid.vaddCommClass_left {M' : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass M'] [VAdd M' β] [VAdd α β] [VAddCommClass M' α β] (S : AddSubmonoid M') : VAddCommClass (↥S) α β

instance Submonoid.smulCommClass_right {M' : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass M'] [SMul α β] [SMul M' β] [SMulCommClass α M' β] (S : Submonoid M') : SMulCommClass α (↥S) β

instance AddSubmonoid.vaddCommClass_right {M' : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass M'] [VAdd α β] [VAdd M' β] [VAddCommClass α M' β] (S : AddSubmonoid M') : VAddCommClass α (↥S) β

instance Submonoid.isScalarTower {M' : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass M'] [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') : IsScalarTower (↥S) α β

Note that this provides IsScalarTower S M' M' which is needed by SMulMulAssoc.

instance AddSubmonoid.vaddAssocClass {M' : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass M'] [VAdd α β] [VAdd M' α] [VAdd M' β] [VAddAssocClass M' α β] (S : AddSubmonoid M') : VAddAssocClass (↥S) α β

theorem Submonoid.smul_def {M' : Type u_1} {α : Type u_2} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : ↥S) (a : α) : g • a = ↑g • a

theorem AddSubmonoid.vadd_def {M' : Type u_1} {α : Type u_2} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : ↥S) (a : α) : g +ᵥ a = ↑g +ᵥ a

@[simp]

theorem Submonoid.mk_smul {M' : Type u_1} {α : Type u_2} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : M') (hg : g ∈ S) (a : α) : ⟨g, hg⟩ • a = g • a

@[simp]

theorem AddSubmonoid.mk_vadd {M' : Type u_1} {α : Type u_2} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : M') (hg : g ∈ S) (a : α) : ⟨g, hg⟩ +ᵥ a = g +ᵥ a

@[instance_reducible]

instance Submonoid.mulAction {M' : Type u_1} {α : Type u_2} [Monoid M'] [MulAction M' α] (S : Submonoid M') : MulAction (↥S) α

The action by a submonoid is the action by the underlying monoid.

Equations

• S.mulAction = inferInstance

@[instance_reducible]

instance AddSubmonoid.addAction {M' : Type u_1} {α : Type u_2} [AddMonoid M'] [AddAction M' α] (S : AddSubmonoid M') : AddAction (↥S) α

The additive action by an AddSubmonoid is the action by the underlying AddMonoid.

Equations

• S.addAction = inferInstance

instance Submonoid.smulDistribClass {M' : Type u_1} {α : Type u_2} {β : Type u_4} {S : Type u_5} [SMul M' α] [SMul M' β] [SMul α β] [SetLike S M'] [h : SMulDistribClass M' α β] (N' : S) : SMulDistribClass (↥N') α β