Theorems · Definition · ring theory

DirectSum.component

(R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      (M : ι → Type w) →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → (i : ι) → (DirectSum ι fun i => M i) →ₗ[R] M i

The projection map onto one component, as a linear map.

Defined in

Mathlib.Algebra.DirectSum.Module

Cited by

16 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule