Theorems · Definition · commutative algebra

Module.compHom

{R : Type u_1} →
  {S : Type u_2} →
    (M : Type u_3) →
      [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → [inst_3 : Semiring S] → (S →+* R) → Module S M

Compose a Module with a RingHom, with action f s • m. See note [reducible non-instances].

Defined in

Mathlib.Algebra.Module.RingHom

Cited by

39 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

SemiringAddCommMonoidModuleSemiring