Theorems · Definition · ring theory

DirectSum.lof

(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 ι] → (i : ι) → M i →ₗ[R] DirectSum ι fun i => M i

Inclusion of each component into the direct sum.

Defined in

Mathlib.Algebra.DirectSum.Module

Cited by

79 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq