sum_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 sum 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 (\sum i ∈ t, f i) ∈ S$$$

Lean4

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

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