Distributive actions by submonoids #
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 = DistribMulAction.compHom α S.subtype
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 = MulDistribMulAction.compHom α S.subtype