{ι : 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')