Theorems · Definition · ring theory

DirectSum.toModule

(R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      {M : ι → Type w} →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [DecidableEq ι] →
              (N : Type u₁) →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] → ((i : ι) → M i →ₗ[R] N) → (DirectSum ι fun i => M i) →ₗ[R] N

The linear map constructed using the universal property of the coproduct.

Defined in

Mathlib.Algebra.DirectSum.Module

Cited by

9 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleDecidableEqAddCommMonoidModule