English
Let G be a commutative group and H a subgroup of G. For any index type ι, a function f from ι to H, and a finite set s of ι, the product of the elements f(i) over i ∈ s, viewed inside H and then embedded into G, equals the product in G of the elements f(i) (taken in G).
Русский
Пусть G — коммутативная группа, H — подгруппа G. Пусть ι — множитель, f: ι → H, s ∈ Finset ι. Произведение f(i) по i∈s, взятое в H и затем включённое в G, равно произведению те же элементов как элементов G.
LaTeX
$$$\uparrow\left(\prod_{i \in s} f(i)\right) = \left(\prod_{i \in s} f(i) : G\right)$$$
Lean4
@[to_additive (attr := simp 1100, norm_cast)]
theorem val_finset_prod {ι G} [CommGroup G] (H : Subgroup G) (f : ι → H) (s : Finset ι) :
↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : G) :=
SubmonoidClass.coe_finset_prod f s
