Theorems · Definition · group theory

AddMonoidHom.pi

{I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → AddZeroClass (f i)] →
      {γ : Type w} → [inst_1 : AddZeroClass γ] → ((i : I) → γ →+ f i) → γ →+ (i : I) → f i

A family of additive monoid homomorphisms f a : γ →+ β a defines a monoid homomorphism Pi.addMonoidHom f : γ →+ Π a, β a given by Pi.addMonoidHom f x b = f b x.

Defined in

Mathlib.Algebra.Group.Pi.Lemmas

Cited by

9 results in Mathlib

Foundations

Depth 13 from the axioms · uses Quot.sound

Assumes

AddZeroClassAddZeroClass