Documentation

Mathlib.Algebra.Group.Submonoid.MulAction

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 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
    @[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
      @[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 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
        @[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
          instance Submonoid.smul {M' : Type u_1} {α : Type u_2} [MulOneClass M'] [SMul M' α] (S : Submonoid M') :
          SMul (↥S) α
          Equations
            instance AddSubmonoid.vadd {M' : Type u_1} {α : Type u_2} [AddZeroClass M'] [VAdd M' α] (S : AddSubmonoid M') :
            VAdd (↥S) α
            Equations
              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 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
                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