multiset_prod_mem — Mathlib

English

Let S be an intermediate field of L over K. If every element of a multiset m of elements of L lies in S, then the product of the elements of m lies in S.

Русский

Пусть S — промежутое поле L над K. Если каждый элемент multiseta m лежит в S, то произведение элементов m лежит в S.

LaTeX

$$$\forall m:\\Multiset L,\ (\forall a \in m,\ a ∈ S) \Rightarrow m.prod ∈ S$$$

Lean4

/-- Product of a multiset of elements in an intermediate field is in the intermediate field. -/
protected theorem multiset_prod_mem (m : Multiset L) : (∀ a ∈ m, a ∈ S) → m.prod ∈ S :=
  multiset_prod_mem m

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