Theorems · Definition · group theory

AddMonoidHom.noncommPiCoprod

{M : Type u_1} →
  [inst : AddMonoid M] →
    {ι : Type u_2} →
      [Fintype ι] →
        {N : ι → Type u_3} →
          [inst_2 : (i : ι) → AddMonoid (N i)] →
            (ϕ : (i : ι) → N i →+ M) →
              (Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)) → ((i : ι) → N i) →+ M

The canonical homomorphism from a family of additive monoids. See also LinearMap.lsum for a linear version without the commutativity assumption.

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

8 results in Mathlib

Foundations

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

Assumes

AddMonoidFintypeAddMonoid