Theorems · Theorem · general algebraic systems

DFinsupp.prod_finset_sum_index

Deprecated since 2026-04-08Use DFinsupp.prod_finsetSum_index instead.

∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {γ : Type w} {α : Type x}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ]
  {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 1) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂) → ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h

Alias of DFinsupp.prod_finsetSum_index.

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidDecidableCommMonoid