coe_finset_prod — Mathlib

English

The product over a Finset of elements of a submonoid, when coerced to the ambient monoid, equals the ambient product.

Русский

Произведение по Finset элементов из подмонома, приведённое в M, равно произведению в M.

LaTeX

$$$\\prod_{i \\in s} (f(i)) = \\left(\\prod_{i \\in s} f(i)\\right)_M$$$

Lean4

@[to_additive (attr := norm_cast, simp)]
theorem coe_finset_prod {ι M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (f : ι → S) (s : Finset ι) :
    ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : M) :=
  map_prod (SubmonoidClass.subtype S) f s

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