list_sum_mem — Mathlib

English

For a subring s of R and a finite list l of elements of R, if every element of l lies in s, then the sum of the elements of l lies in s.

Русский

Для подполья s ⊆ R и конечного списка l элементов R, если каждый элемент из l принадлежит s, то их сумма принадлежит s.

LaTeX

$$$\\forall s:\\ Subring\\,R\\,\\forall l:\\ List\\,R,\\ \\Big(\\forall x \\in l,\\ x \\in s\\Big) \\Rightarrow \\mathrm{sum}(l) \\in s.$$$

Lean4

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

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