prod_pi_mulSingle — Mathlib

English

For a family M i of commutative monoids, ∏ j, Pi.mulSingle j (f j) i = f i.

Русский

Для семейства M i с коммутативными моноидами выполняется: ∏_{j} Pi.mulSingle j (f j) i = f i.

LaTeX

$$$\\displaystyle \\prod_{j} \\Pi.mulSingle j (f j) i = f i$$$

Lean4

/-- See also `Finset.prod_pi_mulSingle`. -/
@[to_additive /-- See also `Finset.sum_pi_single`. -/
    ]
theorem prod_pi_mulSingle {M : ι → Type*} [∀ i, CommMonoid (M i)] (i : ι) (f : ∀ i, M i) :
    ∏ j, Pi.mulSingle j (f j) i = f i :=
  prod_dite_eq _ _

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