coe_finset_prod — Mathlib

English

For a family f: ι → M →* N, the equality of monoid homs holds: the coercion of the Finset product equals the product of the coerced homs.

Русский

Для семейства f: ι → M →* N тождество для моноид-гомомов: преобразование произведения по Finset равно произведению преобразований.

LaTeX

$$$\forall m,\ \left(\prod x \in s, f(x)\right)(m) = \prod x \in s, f(x)(m).$$$

Lean4

@[to_additive]
theorem coe_finset_prod [MulOneClass M] [CommMonoid N] (f : ι → M →* N) (s : Finset ι) :
    ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x) :=
  map_prod (MonoidHom.coeFn M N) _ _

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