Theorems · Theorem · general algebraic systems

DFinsupp.prod_mapRange_index

∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
  [inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] [inst_5 : CommMonoid γ] {f : (i : ι) → β₁ i → β₂ i}
  {hf : ∀ (i : ι), f i 0 = 0} {g : Π₀ (i : ι), β₁ i} {h : (i : ι) → β₂ i → γ},
  (∀ (i : ι), h i 0 = 1) → (DFinsupp.mapRange f hf g).prod h = g.prod fun i b => h i (f i b)

Defined in

Mathlib.Data.DFinsupp.BigOperators

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroZeroDecidableDecidableCommMonoid