Theorems · Inductive type · group theory

MulSemiringActionSemiHomClass

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

MulSemiringActionHomClass F φ R S states that F is a type of morphisms preserving the ring structure and equivariant with respect to φ. You should extend this class when you extend MulSemiringActionHom.

Defined in

Mathlib.GroupTheory.GroupAction.Hom

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

MonoidMonoidSemiringSemiringDistribMulActionDistribMulActionFunLike