Theorems · Definition · group theory

MulSemiringActionHomClass

(F : Type u_15) →
  {M : outParam (Type u_16)} →
    [inst : Monoid M] →
      (R : outParam (Type u_17)) →
        (S : outParam (Type u_18)) →
          [inst_1 : Semiring R] →
            [inst_2 : Semiring S] → [DistribMulAction M R] → [DistribMulAction M S] → [FunLike F R S] → Prop

MulSemiringActionHomClass F M R S states that F is a type of morphisms preserving the ring structure and equivariant with respect to a DistribMulAction of M on R and S.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

MonoidSemiringSemiringDistribMulActionDistribMulActionFunLike