multiset_sum_mem — Mathlib

English

Sum of a multiset of elements in a nonunital subring is in the nonunital subring.

Русский

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

LaTeX

$$$\\forall s: \\text{NonUnitalSubring } R\\, (m: \\text{Multiset } R),\\ (\\forall a \\in m, a \\in s) \\Rightarrow m.sum \\in s$$$

Lean4

/-- Sum of a multiset of elements in a `NonUnitalSubring` of a `NonUnitalRing` is
in the `NonUnitalSubring`. -/
protected theorem multiset_sum_mem {R} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (m : Multiset R) :
    (∀ a ∈ m, a ∈ s) → m.sum ∈ s :=
  multiset_sum_mem _

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