From f65306bd490396052db569fdd959f4e932fd0aca Mon Sep 17 00:00:00 2001
From: "Anne C.A. Baanen" <vierkantor@vierkantor.com>
Date: Thu, 31 Oct 2024 11:58:50 +0100
Subject: [PATCH] Split off a `Ideal/BigOperators.lean` file to avoid
 increasing import count too much.

---
 Mathlib/Algebra/MonoidAlgebra/Ideal.lean      |  3 +-
 Mathlib/RingTheory/Coprime/Ideal.lean         |  1 +
 .../GradedAlgebra/HomogeneousIdeal.lean       |  1 +
 Mathlib/RingTheory/Ideal/Basic.lean           |  4 ---
 Mathlib/RingTheory/Ideal/BigOperators.lean    | 30 +++++++++++++++++++
 Mathlib/RingTheory/ReesAlgebra.lean           |  1 +
 6 files changed, 35 insertions(+), 5 deletions(-)
 create mode 100644 Mathlib/RingTheory/Ideal/BigOperators.lean

diff --git a/Mathlib/Algebra/MonoidAlgebra/Ideal.lean b/Mathlib/Algebra/MonoidAlgebra/Ideal.lean
index 53aaa75a4bf58..26a39f72d9030 100644
--- a/Mathlib/Algebra/MonoidAlgebra/Ideal.lean
+++ b/Mathlib/Algebra/MonoidAlgebra/Ideal.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.MonoidAlgebra.Defs
-import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.BigOperators
+import Mathlib.RingTheory.Ideal.Span
 
 /-!
 # Lemmas about ideals of `MonoidAlgebra` and `AddMonoidAlgebra`
diff --git a/Mathlib/RingTheory/Coprime/Ideal.lean b/Mathlib/RingTheory/Coprime/Ideal.lean
index 3f7176c9ae4c7..8c98a77f7ac7e 100644
--- a/Mathlib/RingTheory/Coprime/Ideal.lean
+++ b/Mathlib/RingTheory/Coprime/Ideal.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pierre-Alexandre Bazin
 -/
 import Mathlib.LinearAlgebra.DFinsupp
+import Mathlib.RingTheory.Ideal.BigOperators
 import Mathlib.RingTheory.Ideal.Operations
 
 /-!
diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean
index a87561a7ee276..33a795a6ea667 100644
--- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean
+++ b/Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Eric Wieser
 -/
 import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.BigOperators
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.RingTheory.GradedAlgebra.Basic
diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean
index c02493e329f22..2ce325801033f 100644
--- a/Mathlib/RingTheory/Ideal/Basic.lean
+++ b/Mathlib/RingTheory/Ideal/Basic.lean
@@ -42,10 +42,6 @@ namespace Ideal
 
 variable [Semiring α] (I : Ideal α) {a b : α}
 
-theorem sum_mem (I : Ideal α) {ι : Type*} {t : Finset ι} {f : ι → α} :
-    (∀ c ∈ t, f c ∈ I) → (∑ i ∈ t, f i) ∈ I :=
-  Submodule.sum_mem I
-
 section Pi
 
 variable (ι : Type v)
diff --git a/Mathlib/RingTheory/Ideal/BigOperators.lean b/Mathlib/RingTheory/Ideal/BigOperators.lean
new file mode 100644
index 0000000000000..a1f292757e816
--- /dev/null
+++ b/Mathlib/RingTheory/Ideal/BigOperators.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Chris Hughes, Mario Carneiro
+-/
+import Mathlib.Algebra.Module.Submodule.Basic
+import Mathlib.RingTheory.Ideal.Defs
+
+/-!
+
+# Big operators for ideals
+
+This contains some results on the big operators `∑` and `∏` interacting with the `Ideal` type.
+-/
+
+
+universe u v w
+
+variable {α : Type u} {β : Type v} {F : Type w}
+
+namespace Ideal
+
+variable [Semiring α] (I : Ideal α) {a b : α}
+
+theorem sum_mem (I : Ideal α) {ι : Type*} {t : Finset ι} {f : ι → α} :
+    (∀ c ∈ t, f c ∈ I) → (∑ i ∈ t, f i) ∈ I :=
+  Submodule.sum_mem I
+
+end Ideal
+
diff --git a/Mathlib/RingTheory/ReesAlgebra.lean b/Mathlib/RingTheory/ReesAlgebra.lean
index 6fe710e881b77..1804becca9c77 100644
--- a/Mathlib/RingTheory/ReesAlgebra.lean
+++ b/Mathlib/RingTheory/ReesAlgebra.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
+import Mathlib.RingTheory.Ideal.BigOperators
 import Mathlib.RingTheory.FiniteType
 
 /-!