multiset_prod_mem — Mathlib

English

If every element of a multiset m lies in a Subsemiring s of a commutative semiring, then the product of all elements of m lies in s.

Русский

Если каждый элемент мультисовета m принадлежит Subsemiring s ⊆ R, то произведение всех элементов m принадлежит s.

LaTeX

$${m : Multiset R} → (∀ a ∈ m, a ∈ s) → m.prod ∈ s$$

Lean4

/-- Product of a multiset of elements in a `Subsemiring` of a `CommSemiring`
is in the `Subsemiring`. -/
protected theorem multiset_prod_mem {R} [CommSemiring R] (s : Subsemiring R) (m : Multiset R) :
    (∀ a ∈ m, a ∈ s) → m.prod ∈ s :=
  multiset_prod_mem m

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