Theorems · Theorem · group theory

list_sum_mem

∀ {M : Type u_1} {B : Type u_3} [inst : AddMonoid M] [inst_1 : SetLike B M] [AddSubmonoidClass B M] {S : B}
  {l : List M}, (∀ x ∈ l, x ∈ S) → l.sum ∈ S

Sum of a list of elements in an AddSubmonoid is in the AddSubmonoid.

Defined in

Mathlib.Algebra.Group.Submonoid.BigOperators

Cited by

10 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidSetLikeAddSubmonoidClass