prod_fiberwise — Mathlib

English

Let g: ι → κ be a function and f: ι → M. Then the product over j of the product over i with g i = j of f i equals the product over i of f i.

Русский

Пусть g: ι → κ и f: ι → M. Тогда произведение по j от произведения по i с g(i)=j f(i) равно произведению по i от f(i).

LaTeX

$$$$\\prod_{j} \\left( \\prod_{i : g(i)=j} f(i) \\right) = \\prod_{i} f(i)$$$$

Lean4

@[to_additive]
theorem prod_fiberwise [DecidableEq κ] (g : ι → κ) (f : ι → M) : ∏ j, ∏ i : { i // g i = j }, f i = ∏ i, f i :=
  by
  rw [← Finset.prod_fiberwise _ g f]
  congr with j
  exact (prod_subtype _ (by simp) _).symm

Похожие утверждения