prod_mem — Mathlib

English

Let S be an intermediate field of L over K. For any finite index set ι, any function f: ι → L, if each f(i) ∈ S for i in a finite set t, then the product over i ∈ t of f(i) lies in S.

Русский

Пусть S — промежутое поле L над K. Для конечного индекса ι и функции f:ι→L, если каждый f(i) ∈ S для i ∈ t, то произведение по i∈t равно ∏ f(i) ∈ S.

LaTeX

$$$\forall ι\, {t : Finset ι}\, {f : ι → L},\ (\forall i ∈ t,\ f i ∈ S) \Rightarrow (\prod i ∈ t, f i) ∈ S$$$

Lean4

/-- Product of elements of an intermediate field indexed by a `Finset` is in the intermediate field.
-/
protected theorem prod_mem {ι : Type*} {t : Finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) : (∏ i ∈ t, f i) ∈ S :=
  prod_mem h

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