# Distributive actions by submonoids #

source
@[instance 100]
instance Submonoid.instDistribMulActionSubtypeMem {M : Type u_1} {α : Type u_2} [Monoid M] {S : Type u_3} [SetLike S M] (s : S) [SubmonoidClass S M] [AddMonoid α] [DistribMulAction M α] :
DistribMulAction (↥s) α
Equations

- Submonoid.instDistribMulActionSubtypeMem s = { toMulAction := Submonoid.instMulActionSubtypeMem s, smul_zero := ⋯, smul_add := ⋯ }

source
instance Submonoid.distribMulAction {M : Type u_1} {α : Type u_2} [Monoid M] [AddMonoid α] [DistribMulAction M α] (S : Submonoid M) :
DistribMulAction (↥S) α

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

Equations

- S.distribMulAction = inferInstance

source
@[instance 100]
instance Submonoid.instMulDistribMulActionSubtypeMem {M : Type u_1} {α : Type u_2} [Monoid M] {S : Type u_3} [SetLike S M] (s : S) [SubmonoidClass S M] [Monoid α] [MulDistribMulAction M α] :
MulDistribMulAction (↥s) α
Equations

- Submonoid.instMulDistribMulActionSubtypeMem s = { toMulAction := Submonoid.instMulActionSubtypeMem s, smul_mul := ⋯, smul_one := ⋯ }

source
instance Submonoid.mulDistribMulAction {M : Type u_1} {α : Type u_2} [Monoid M] [Monoid α] [MulDistribMulAction M α] (S : Submonoid M) :
MulDistribMulAction (↥S) α

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

Equations

- S.mulDistribMulAction = inferInstance