Theorems · Definition · group theory

DirectSum.coeAddMonoidHom

{ι : Type v} →
  {M : Type u_1} →
    {S : Type u_2} →
      [DecidableEq ι] →
        [inst : AddCommMonoid M] →
          [inst_1 : SetLike S M] → [inst_2 : AddSubmonoidClass S M] → (A : ι → S) → (DirectSum ι fun i => ↥(A i)) →+ M

The canonical embedding from ⨁ i, A i to M where A is a collection of AddSubmonoid M indexed by ι. When S = Submodule _ M, this is available as a LinearMap, DirectSum.coe_linearMap.

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidSetLikeAddSubmonoidClass