English
Let M be a commutative monoid. If S is a submonoid and t is a finite set of indices with f(i) ∈ S for all i ∈ t, then the product ∏_{i∈t} f(i) lies in S.
Русский
Пусть M — коммутативный моноид. Если S — подмономод, t — конечный набор индексов и f(i) ∈ S для каждого i ∈ t, то произведение ∏_{i∈t} f(i) ∈ S.
LaTeX
$$$$ \\left( \\prod_{c \\in t} f(c) \\right) \\in S $$$$
Lean4
/-- Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the
submonoid. -/
@[to_additive /-- Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset`
is in the `AddSubmonoid`. -/
]
theorem prod_mem {M : Type*} [CommMonoid M] (S : Submonoid M) {ι : Type*} {t : Finset ι} {f : ι → M}
(h : ∀ c ∈ t, f c ∈ S) : (∏ c ∈ t, f c) ∈ S :=
S.multiset_prod_mem (t.1.map f) fun _ hx =>
let ⟨i, hi, hix⟩ := Multiset.mem_map.1 hx
hix ▸ h i hi
