Theorems · Definition · group theory

MonoidHom.pi

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

A family of monoid homomorphisms f a : γ →* β a defines a monoid homomorphism Pi.monoidHom f : γ →* Π a, β a given by Pi.monoidHom 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

MulOneClassMulOneClass