Theorems · Definition · group theory

Pi.monoidHom

Deprecated since 2026-05-29Use MonoidHom.pi instead.

{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

Alias of MonoidHom.pi. 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

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

MulOneClassMulOneClass