Theorems · Definition · group theory

Pi.monoidHomMulEquiv

{ι : Type u_7} →
  [Fintype ι] →
    [DecidableEq ι] →
      (M : ι → Type u_8) →
        [inst : (i : ι) → CommMonoid (M i)] →
          (M' : Type u_9) → [inst_1 : CommMonoid M'] → (((i : ι) → M i) →* M') ≃* ((i : ι) → M i →* M')

The canonical isomorphism between the monoid of homomorphisms from a finite product of commutative monoids to another commutative monoid and the product of the homomorphism monoids.

Defined in

Mathlib.Algebra.BigOperators.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommMonoidCommMonoid