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.finsuppSum_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : Type u_3} [Zero β] {f : ι →₀ β} (g : ι → β → R) (h : ∀ i ∈ f.support, g i (f i) ∈ I) : f.sum g ∈ I

theorem TwoSidedIdeal.dfinsuppSum_mem {R : Type u_1} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : ι → Type u_3} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} (g : (i : ι) → β i → R) (h : ∀ i ∈ f.support, g i (f i) ∈ I) : f.sum g ∈ 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

theorem TwoSidedIdeal.finsuppProd_mem {R : Type u_1} [CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : Type u_3} {M : Type u_4} [Add M] [CommMonoid M] [Zero β] (h : ι → β → R) {f : ι →₀ β} (H : ∃ i ∈ f.support, h i (f i) ∈ I) : f.prod h ∈ I

theorem TwoSidedIdeal.dfinsuppProd_mem {R : Type u_1} [CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : ι → Type u_3} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} (g : (i : ι) → β i → R) (h : ∃ i ∈ f.support, g i (f i) ∈ I) : f.prod g ∈ I