Distributive actions by submonoids #
@[instance_reducible, 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_reducible]
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
@[instance_reducible, 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_one := ⋯, smul_mul := ⋯ }
@[instance_reducible]
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.