# Instances of `MulSemiringAction`

for subobjects #

These are defined in this file as `Semiring`

s are not available yet where `Submonoid`

and `Subgroup`

are defined.

Instances for `Subsemiring`

and `Subring`

are provided next to the other scalar actions instances
for those subobjects.

instance
Submonoid.mulSemiringAction
{M : Type u_1}
{R : Type u_3}
[Monoid M]
[Semiring R]
[MulSemiringAction M R]
(H : Submonoid M)
:

MulSemiringAction { x // x ∈ H } R

A stronger version of `Submonoid.distribMulAction`

.

instance
Subgroup.mulSemiringAction
{G : Type u_2}
{R : Type u_3}
[Group G]
[Semiring R]
[MulSemiringAction G R]
(H : Subgroup G)
:

MulSemiringAction { x // x ∈ H } R

A stronger version of `Subgroup.distribMulAction`

.