Module docstring
{"# Big operators for ideals
This contains some results on the big operators ∑ and ∏ interacting with the Ideal type.
"}
Ideal.sum_mem
theorem
(I : Ideal α) {ι : Type*} {t : Finset ι} {f : ι → α} : (∀ c ∈ t, f c ∈ I) → (∑ i ∈ t, f i) ∈ I
Full source
theorem sum_mem (I : Ideal α) {ι : Type*} {t : Finset ι} {f : ι → α} :
(∀ c ∈ t, f c ∈ I) → (∑ i ∈ t, f i) ∈ I :=
Submodule.sum_mem IInformal description
Let $I$ be an ideal in a commutative ring $\alpha$, $\iota$ be a type, $t$ a finite set of elements of $\iota$, and $f : \iota \to \alpha$ a function. If for every $c \in t$ we have $f(c) \in I$, then the sum $\sum_{i \in t} f(i)$ belongs to $I$.