Split off a Ideal/BigOperators.lean file to avoid increasing import…

… count too much.
leanprover-community · Oct 31, 2024 · f65306b · f65306b
1 parent 272748f
commit f65306b
Show file tree

Hide file tree

Showing 6 changed files with 35 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
 
 /-!