multiset_sum_mem — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall R\\, [\\text{Ring }R]\\, (s: Subring R)\\, (m: Multiset R),\\ (\\forall a \\in m, a \\in s) \\Rightarrow m.sum \\in s.$$$

Lean4

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

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