list_sum_mem — Mathlib

English

Sum of a list of elements in a nonunital subring is again in the same nonunital subring.

Русский

Сумма элементов списка в неумножающем подкольце снова принадлежит этому подкольцу.

LaTeX

$$$\\forall s: \\text{NonUnitalSubring } R\\, (\\text{list } l),\\ (\\forall x \\in l, x \\in s) \\Rightarrow l_{sum} \\in s$$$

Lean4

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

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