Theorems · Definition · group theory

DirectSum.map

{ι : Type u_3} →
  {α : ι → Type u_4} →
    {β : ι → Type u_5} →
      [inst : (i : ι) → AddCommMonoid (α i)] →
        [inst_1 : (i : ι) → AddCommMonoid (β i)] →
          ((i : ι) → α i →+ β i) → (DirectSum ι fun i => α i) →+ DirectSum ι fun i => β i

create a homomorphism from ⨁ i, α i to ⨁ i, β i by giving the component-wise map f.

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid