Distributive actions by submonoids

@[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 := ⋯ }

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

@[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 := ⋯ }

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