English
Product over a finite set t of elements in a subgroup K lies in K, provided each factor lies in K.
Русский
Произведение по конечному набору элементов t, каждый элемент которых лежит в K, принадлежит K.
LaTeX
$$$\\forall c \\in t, f(c) \\in K \\Rightarrow \\prod_{c \\in t} f(c) \\in K$$$
Lean4
/-- Product of elements of a subgroup of a `CommGroup` indexed by a `Finset` is in the
subgroup. -/
@[to_additive /-- Sum of elements in an `AddSubgroup` of an `AddCommGroup` indexed by a `Finset`
is in the `AddSubgroup`. -/
]
protected theorem prod_mem {G : Type*} [CommGroup G] (K : Subgroup G) {ι : Type*} {t : Finset ι} {f : ι → G}
(h : ∀ c ∈ t, f c ∈ K) : (∏ c ∈ t, f c) ∈ K :=
prod_mem h
