Documentation

Mathlib.Algebra.Ring.Action.Subobjects

Instances of MulSemiringAction for subobjects #

These are defined in this file as Semirings 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.

source
@[instance 100]
instance instMulSemiringActionSubtypeMem {M : Type u_1} {R : Type u_3} [Monoid M] [Semiring R] [MulSemiringAction M R] {S : Type u_4} [SetLike S M] (s : S) [SubmonoidClass S M] :
MulSemiringAction (↥s) R
Equations
source
instance Submonoid.mulSemiringAction {M : Type u_1} {R : Type u_3} [Monoid M] [Semiring R] [MulSemiringAction M R] (H : Submonoid M) :
MulSemiringAction (↥H) R

A stronger version of Submonoid.distribMulAction.

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

A stronger version of Subgroup.distribMulAction.

Equations