Interactions between ∑, ∏ and two sided ideals

theorem TwoSidedIdeal.listSum_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (l : List ι) (f : ι → R) (hl : ∀ x ∈ l, f x ∈ I) : (List.map f l).sum ∈ I

theorem TwoSidedIdeal.multisetSum_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Multiset ι) (f : ι → R) (hs : ∀ x ∈ s, f x ∈ I) : (Multiset.map f s).sum ∈ I

theorem TwoSidedIdeal.finsetSum_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Finset ι) (f : ι → R) (hs : ∀ x ∈ s, f x ∈ I) : s.sum f ∈ I

theorem TwoSidedIdeal.listProd_mem {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) {ι : Type u_2} (l : List ι) (f : ι → R) (hl : ∃ x ∈ l, f x ∈ I) : (List.map f l).prod ∈ I

theorem TwoSidedIdeal.multiSetProd_mem {R : Type u_1} [CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Multiset ι) (f : ι → R) (hs : ∃ x ∈ s, f x ∈ I) : (Multiset.map f s).prod ∈ I

theorem TwoSidedIdeal.finsetProd_mem {R : Type u_1} [CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Finset ι) (f : ι → R) (hs : ∃ x ∈ s, f x ∈ I) : s.prod f ∈ I