# 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_2}
[inst : Monoid M]
[inst : Semiring R]
[inst : MulSemiringAction M R]
(H : Submonoid M)
:

MulSemiringAction { x // x ∈ H } R

A stronger version of `Submonoid.distribMulAction`

.

## Equations

- One or more equations did not get rendered due to their size.

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

MulSemiringAction { x // x ∈ H } R

A stronger version of `Subgroup.distribMulAction`

.

## Equations

- Subgroup.mulSemiringAction H = Submonoid.mulSemiringAction H.toSubmonoid