chore: remove some unnecessary 'open BigOperators' (#11880)

Could we have an `open` linter, that checked for unused opened namespaces? Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Apr 4, 2024 · 16eb4bd · 16eb4bd
1 parent 6d89490
commit 16eb4bd
Show file tree

Hide file tree

Showing 13 changed files with 5 additions and 23 deletions.
diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
@@ -94,8 +94,6 @@ the second approach only when you need to weaken a condition on either `R` or `A
 
 universe u v w u₁ v₁
 
-open BigOperators
-
 section Prio
 
 -- We set this priority to 0 later in this file

diff --git a/Mathlib/Algebra/Category/GroupCat/Biproducts.lean b/Mathlib/Algebra/Category/GroupCat/Biproducts.lean
@@ -20,8 +20,6 @@ open CategoryTheory
 
 open CategoryTheory.Limits
 
-open BigOperators
-
 universe w u
 
 namespace AddCommGroupCat

diff --git a/Mathlib/Algebra/CharP/Reduced.lean b/Mathlib/Algebra/CharP/Reduced.lean
@@ -15,8 +15,6 @@ import Mathlib.RingTheory.Nilpotent
 
 open Finset
 
-open BigOperators
-
 section
 
 variable (R : Type*) [CommRing R] [IsReduced R] (p n : ℕ) [ExpChar R p]

diff --git a/Mathlib/Algebra/Lie/EngelSubalgebra.lean b/Mathlib/Algebra/Lie/EngelSubalgebra.lean
@@ -30,7 +30,7 @@ and minimal ones are nilpotent (TODO), hence Cartan subalgebras.
   if it is contained in the Engel subalgebra of all its elements.
 -/
 
-open BigOperators LieAlgebra LieModule
+open LieAlgebra LieModule
 
 variable {R L M : Type*} [CommRing R] [LieRing L] [LieAlgebra R L]
   [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]

diff --git a/Mathlib/Algebra/Module/Submodule/Bilinear.lean b/Mathlib/Algebra/Module/Submodule/Bilinear.lean
@@ -29,8 +29,6 @@ universe uι u v
 
 open Set
 
-open BigOperators
-
 open Pointwise
 
 namespace Submodule

diff --git a/Mathlib/Algebra/Module/Submodule/Ker.lean b/Mathlib/Algebra/Module/Submodule/Ker.lean
@@ -29,7 +29,7 @@ linear algebra, vector space, module
 
 open Function
 
-open BigOperators Pointwise
+open Pointwise
 
 variable {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
 variable {K : Type*}

diff --git a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean
@@ -157,7 +157,7 @@ derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor ser
 noncomputable section
 
 open scoped Classical
-open BigOperators NNReal Topology Filter
+open NNReal Topology Filter
 
 local notation "∞" => (⊤ : ℕ∞)
 

diff --git a/Mathlib/Analysis/Calculus/Deriv/Add.lean b/Mathlib/Analysis/Calculus/Deriv/Add.lean
@@ -148,9 +148,6 @@ section Sum
 
 /-! ### Derivative of a finite sum of functions -/
 
-
-open BigOperators
-
 variable {ι : Type*} {u : Finset ι} {A : ι → 𝕜 → F} {A' : ι → F}
 
 theorem HasDerivAtFilter.sum (h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) x L) :

diff --git a/Mathlib/Analysis/Complex/TaylorSeries.lean b/Mathlib/Analysis/Complex/TaylorSeries.lean
@@ -26,7 +26,7 @@ see `Complex.hasSum_taylorSeries_of_entire`, `Complex.taylorSeries_eq_of_entire`
 
 namespace Complex
 
-open BigOperators Nat
+open Nat
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄
 

diff --git a/Mathlib/Analysis/Convex/Join.lean b/Mathlib/Analysis/Convex/Join.lean
@@ -18,8 +18,6 @@ convex hulls of finite sets.
 
 open Set
 
-open BigOperators
-
 variable {ι : Sort*} {𝕜 E : Type*}
 
 section OrderedSemiring

diff --git a/Mathlib/Analysis/LocallyConvex/AbsConvex.lean b/Mathlib/Analysis/LocallyConvex/AbsConvex.lean
@@ -38,7 +38,7 @@ disks, convex, balanced
 
 open NormedField Set
 
-open BigOperators NNReal Pointwise Topology
+open NNReal Pointwise Topology
 
 variable {𝕜 E F G ι : Type*}
 

diff --git a/Mathlib/Analysis/NormedSpace/Int.lean b/Mathlib/Analysis/NormedSpace/Int.lean
@@ -19,8 +19,6 @@ The resulting nonnegative real number is denoted by `‖n‖₊`.
 -/
 
 
-open BigOperators
-
 namespace Int
 
 theorem nnnorm_coe_units (e : ℤˣ) : ‖(e : ℤ)‖₊ = 1 := by

diff --git a/Mathlib/CategoryTheory/Linear/FunctorCategory.lean b/Mathlib/CategoryTheory/Linear/FunctorCategory.lean
@@ -16,9 +16,6 @@ then `C ⥤ D` is also `R`-linear.
 
 -/
 
-
-open BigOperators
-
 namespace CategoryTheory
 
 open CategoryTheory.Limits Linear