finset_prod_singleton — Mathlib

English

The product over a Finset of singleton sets equals the singleton of the product.

Русский

Произведение по Finset одиночных множеств равно единственному множеству произведения.

LaTeX

$$Finset.prod (fun i => { I i }) = { Finset.prod (fun i => I i) }$$

Lean4

@[to_additive]
theorem finset_prod_singleton {M ι : Type*} [CommMonoid M] (s : Finset ι) (I : ι → M) :
    ∏ i ∈ s, ({I i} : Set M) = {∏ i ∈ s, I i} :=
  (map_prod (singletonMonoidHom : M →* Set M) _ _).symm

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