multiset_prod_mem — Mathlib

English

If a finite collection of elements all lie in a subfield s of a field K, then their product lies in s.

Русский

Если элементы множества принадлежат подполью s ⊆ K, то их произведение принадлежит s.

LaTeX

$$$ \\forall a\\in m,\ a\\in s \\Rightarrow m.\\mathrm{prod}\ a \\in s $$$

Lean4

/-- Product of a multiset of elements in a subfield is in the subfield. -/
protected theorem multiset_prod_mem (m : Multiset K) : (∀ a ∈ m, a ∈ s) → m.prod ∈ s :=
  multiset_prod_mem m

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