sum_mem — Mathlib

English

Sum of a subring of a ring indexed by a finite set is in the subring.

Русский

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

LaTeX

$$$\\forall R\\, [\\text{Ring }R]\\, (s: Subring R)\\, (t: Finset\\, ι)\\, (f: ι \\to R),\\ (\\forall c \\in t, f c \\in s) \\Rightarrow (\\sum i \\in t, f i) \\in s.$$$

Lean4

/-- Sum of elements in a `Subring` of a `Ring` indexed by a `Finset`
is in the `Subring`. -/
protected theorem sum_mem {R : Type*} [Ring R] (s : Subring R) {ι : Type*} {t : Finset ι} {f : ι → R}
    (h : ∀ c ∈ t, f c ∈ s) : (∑ i ∈ t, f i) ∈ s :=
  sum_mem h

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