Theorems · Definition · group theory

DirectSum.toAddMonoid

{ι : Type v} →
  {β : ι → Type w} →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      [DecidableEq ι] →
        {γ : Type u₁} → [inst_2 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) → (DirectSum ι fun i => β i) →+ γ

toAddMonoid φ is the natural homomorphism from ⨁ i, β i to γ induced by a family φ of homomorphisms β i → γ.

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEqAddCommMonoid