multiset_prod_mem — Mathlib

English

If every element of a multiset lies in S, then the product of its elements lies in S.

Русский

Если каждый элемент мультинабора принадлежит S, то их произведение принадлежит S.

LaTeX

$$$$ \\forall m:\\\\text{Multiset}(A),\\ (\\\\forall x\\\\in m,\\ x\\\\in S)\\\\Rightarrow m.prod\\\\in S $$$$

Lean4

protected theorem multiset_prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A]
    (S : Subalgebra R A) {m : Multiset A} (h : ∀ x ∈ m, x ∈ S) : m.prod ∈ S :=
  multiset_prod_mem m h

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