English
Let R be a (not necessarily unital) nonunital ring and S a nonunital subring of R. For any finite index set ι, any function f: ι → R, if f(i) ∈ S for all i ∈ t, then the finite sum ∑_{i∈t} f(i) lies in S.
Русский
Пусть R — кольцо без единицы и S — подпольное кольцо без единицы в R. Пусть t — конечный подмножество индексов и f: t → R такая, что для всех i ∈ t выполняется f(i) ∈ S. Тогда сумма ∑_{i∈t} f(i) принадлежит S.
LaTeX
$$$\\\\forall t: \\\\mathrm{Finset}\, \\\\iota, \\\\forall f: \\\\iota \to R, (\\\\forall i \\\\in t, f i \\in s) \\Rightarrow \\\\sum_{i \\\\in t} f i \\in s$$$
Lean4
/-- Sum of elements in a `NonUnitalSubring` of a `NonUnitalRing` indexed by a `Finset`
is in the `NonUnitalSubring`. -/
protected theorem sum_mem {R : Type*} [NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {ι : Type*} {t : Finset ι}
{f : ι → R} (h : ∀ c ∈ t, f c ∈ s) : (∑ i ∈ t, f i) ∈ s :=
sum_mem h
