list_prod_mem — Mathlib

English

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

Русский

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

LaTeX

$$$\forall l:\\List L,\ (\forall x \in l,\ x \in S) \Rightarrow l.prod ∈ S$$$

Lean4

/-- Product of a list of elements in an intermediate field is in the intermediate field. -/
protected theorem list_prod_mem {l : List L} : (∀ x ∈ l, x ∈ S) → l.prod ∈ S :=
  list_prod_mem

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