list_sum_mem — Mathlib

English

If every element of a finite list l lies in a subfield s, then the sum of the list lies in s.

Русский

Если все элементы конечного списка l принадлежат подполю s, то сумма элементов l принадлежит s.

LaTeX

$$$ \Bigl( \forall x \in l, x \in s \Bigr) \rightarrow l.\text{sum} \in s $$$

Lean4

/-- Sum of a list of elements in a subfield is in the subfield. -/
protected theorem list_sum_mem {l : List K} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s :=
  list_sum_mem

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