Documentation

Mathlib.Algebra.Group.Submonoid.DistribMulAction

Distributive actions by submonoids #

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

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

Equations
instance Submonoid.mulDistribMulAction {M : Type u_1} {α : Type u_2} [Monoid M] [Monoid α] [MulDistribMulAction M α] (S : Submonoid M) :
MulDistribMulAction { x : M // x S } α

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

Equations