English
Product over a Finset of elements f c in a submonoid S lies in S if each f c ∈ S.
Русский
Произведение по Finset элементов f c, принадлежащих подмоном S, лежит в S.
LaTeX
$$$\\forall c \\in t, f(c) \\in S \\Rightarrow \\prod_{c \\in t} f(c) \\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] [SetLike B M] [SubmonoidClass B M] {ι : Type*} {t : Finset ι} {f : ι → M}
(h : ∀ c ∈ t, f c ∈ S) : (∏ c ∈ t, f c) ∈ S :=
multiset_prod_mem (t.1.map f) fun _x hx =>
let ⟨i, hi, hix⟩ := Multiset.mem_map.1 hx
hix ▸ h i hi
