prod_sigma_eq_prod — Mathlib

English

A reindexing identity: the product over the partition pieces equals the product over all indices: ∏_{m} ∏_{r} v(c.emb m r) = ∏_{i} v(i).

Русский

Переприведение индексов: произведение по частям разбиения равно произведению по всем индексам.

LaTeX

$$$\\prod_{m:\\mathrm{Fin}(c.length)} \\; \\prod_{r:\\mathrm{Fin}(c.partSize m)} v( c.emb m r ) = \\prod_{i} v(i)$$$

Lean4

@[to_additive]
theorem prod_sigma_eq_prod {α : Type*} [CommMonoid α] (v : Fin n → α) :
    ∏ (m : Fin c.length), ∏ (r : Fin (c.partSize m)), v (c.emb m r) = ∏ i, v i :=
  by
  rw [Finset.prod_sigma']
  exact Fintype.prod_equiv c.equivSigma _ _ (fun p ↦ rfl)

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