Theorems · Definition · group theory

AddMonoidHom.piMap

{ι : Type u_1} →
  {M : ι → Type u_3} →
    {N : ι → Type u_4} →
      [inst : (i : ι) → AddZeroClass (M i)] →
        [inst_1 : (i : ι) → AddZeroClass (N i)] → ((i : ι) → M i →+ N i) → ((i : ι) → M i) →+ (i : ι) → N i

A family of additive monoid homomorphisms f i : M i →+ N i defines an additive monoid homomorphism AddMonoidHom.piMap f : (Π i, M i) →+ (Π i, N i) given by AddMonoidHom.piMap f x i = f i x. This is Pi.map for AddMonoidHoms.

Defined in

Mathlib.Algebra.Group.Pi.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

AddZeroClassAddZeroClass