Big operators for ideals

This contains some results on the big operators ∑ and ∏ interacting with the Ideal type.

theorem Ideal.sum_mem {α : Type u} [Semiring α] (I : Ideal α) {ι : Type u_1} {t : Finset ι} {f : ι → α} : (∀ c ∈ t, f c ∈ I) → ∑ i ∈ t, f i ∈ I