Theorems · Definition · ring theory

MulSemiringAction.compHom

{M : Type u_1} →
  {N : Type u_2} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] →
        (R : Type v) → [inst_2 : Semiring R] → (N →* M) → [MulSemiringAction M R] → MulSemiringAction N R

Compose a MulSemiringAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

Defined in

Mathlib.Algebra.Ring.Action.Basic

Cited by

2 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

MonoidMonoidSemiringMulSemiringAction