chore: scoped BigOperators notation (#1952)

leanprover-community · Jan 30, 2023 · e707fa6 · e707fa6
1 parent c73daed
commit e707fa6
Show file tree

Hide file tree

Showing 44 changed files with 58 additions and 86 deletions.
diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -28,7 +28,7 @@ In this file we define products and sums indexed by finite sets (specifically, `
 ## Notation
 
 We introduce the following notation, localized in `BigOperators`.
-To enable the notation, use `open_locale BigOperators`.
+To enable the notation, use `open BigOperators`.
 
 Let `s` be a `Finset α`, and `f : α → β` a function.
 
@@ -100,39 +100,40 @@ In practice, this means that parentheses should be placed as follows:
 (Example taken from page 490 of Knuth's *Concrete Mathematics*.)
 -/
 
-section
+-- TODO: Use scoped[NS], when implemented?
+namespace BigOperators
 open Std.ExtendedBinder
 
 /-- `∑ x, f x` is notation for `Finset.sum Finset.univ f`. It is the sum of `f x`,
 where `x` ranges over the finite domain of `f`. -/
-syntax (name := bigsum) "∑ " extBinder ", " term:67 : term
-macro_rules (kind := bigsum)
+scoped syntax (name := bigsum) "∑ " extBinder ", " term:67 : term
+scoped macro_rules (kind := bigsum)
   | `(∑ $x:ident, $p) => `(Finset.sum Finset.univ (fun $x:ident ↦ $p))
   | `(∑ $x:ident : $t, $p) => `(Finset.sum Finset.univ (fun $x:ident : $t ↦ $p))
 
 /-- `∏ x, f x` is notation for `Finset.prod Finset.univ f`. It is the product of `f x`,
 where `x` ranges over the finite domain of `f`. -/
-syntax (name := bigprod) "∏ " extBinder ", " term:67 : term
-macro_rules (kind := bigprod)
+scoped syntax (name := bigprod) "∏ " extBinder ", " term:67 : term
+scoped macro_rules (kind := bigprod)
   | `(∏ $x:ident, $p) => `(Finset.prod Finset.univ (fun $x:ident ↦ $p))
   | `(∏ $x:ident : $t, $p) => `(Finset.prod Finset.univ (fun $x:ident : $t ↦ $p))
 
 /-- `∑ x in s, f x` is notation for `Finset.sum s f`. It is the sum of `f x`,
 where `x` ranges over the finite set `s`. -/
-syntax (name := bigsumin) "∑ " extBinder "in " term "," term:67 : term
-macro_rules (kind := bigsumin)
+scoped syntax (name := bigsumin) "∑ " extBinder "in " term "," term:67 : term
+scoped macro_rules (kind := bigsumin)
   | `(∑ $x:ident in $s, $r) => `(Finset.sum $s (fun $x ↦ $r))
   | `(∑ $x:ident : $t in $s, $p) => `(Finset.sum $s (fun $x:ident : $t ↦ $p))
 
 /-- `∏ x, f x` is notation for `Finset.prod s f`. It is the sum of `f x`,
 where `x` ranges over the finite set `s`. -/
-syntax (name := bigprodin) "∏ " extBinder "in " term "," term:67 : term
-macro_rules (kind := bigprodin)
+scoped syntax (name := bigprodin) "∏ " extBinder "in " term "," term:67 : term
+scoped macro_rules (kind := bigprodin)
   | `(∏ $x:ident in $s, $r) => `(Finset.prod $s (fun $x ↦ $r))
   | `(∏ $x:ident : $t in $s, $p) => `(Finset.prod $s (fun $x:ident : $t ↦ $p))
-end
+end BigOperators
 
--- open BigOperators -- Porting note: commented out locale
+open BigOperators
 
 namespace Finset
 

diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -85,8 +85,7 @@ section sort
 
 variable {G M N : Type _} {α β ι : Sort _} [CommMonoid M] [CommMonoid N]
 
--- Porting note: Unknown namespace BigOperators
---open BigOperators
+open BigOperators
 
 section
 
@@ -369,8 +368,7 @@ section type
 
 variable {α β ι G M N : Type _} [CommMonoid M] [CommMonoid N]
 
--- Porting note: Unknown namespace
---open BigOperators
+open BigOperators
 
 @[to_additive]
 theorem finprod_eq_mulIndicator_apply (s : Set α) (f : α → M) (a : α) :

diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean
@@ -25,8 +25,7 @@ noncomputable section
 
 open Finset Function
 
--- Porting note: Unkonwn namespace BigOperators
--- open BigOperators
+open BigOperators
 
 variable {α ι γ A B C : Type _} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C]
 

diff --git a/Mathlib/Algebra/BigOperators/Intervals.lean b/Mathlib/Algebra/BigOperators/Intervals.lean
@@ -22,7 +22,7 @@ We prove results about big operators over intervals (mostly the `ℕ`-valued `Ic
 
 universe u v w
 
--- open BigOperators -- porting note: notation is global for now
+open BigOperators
 open Nat
 
 namespace Finset

diff --git a/Mathlib/Algebra/BigOperators/NatAntidiagonal.lean b/Mathlib/Algebra/BigOperators/NatAntidiagonal.lean
@@ -17,8 +17,7 @@ import Mathlib.Algebra.BigOperators.Basic
 This file contains theorems relevant to big operators over `Finset.NatAntidiagonal`.
 -/
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 variable {M N : Type _} [CommMonoid M] [AddCommMonoid N]
 

diff --git a/Mathlib/Algebra/BigOperators/Option.lean b/Mathlib/Algebra/BigOperators/Option.lean
@@ -18,8 +18,7 @@ In this file we prove formulas for products and sums over `Finset.insertNone s`
 `Finset.eraseNone s`.
 -/
 
--- Porting note: big operators are currently global
---open BigOperators
+open BigOperators
 
 open Function
 

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
@@ -22,8 +22,7 @@ Mostly monotonicity results for the `∏` and `∑` operations.
 
 open Function
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 variable {ι α β M N G k R : Type _}
 

diff --git a/Mathlib/Algebra/BigOperators/Pi.lean b/Mathlib/Algebra/BigOperators/Pi.lean
@@ -21,8 +21,7 @@ of monoids and groups
 -/
 
 
--- Port note: commented out the next line
--- open BigOperators
+open BigOperators
 
 namespace Pi
 

diff --git a/Mathlib/Algebra/BigOperators/Ring.lean b/Mathlib/Algebra/BigOperators/Ring.lean
@@ -23,7 +23,7 @@ multiplicative and additive structures on the values being combined.
 
 universe u v w
 
--- open BigOperators -- Porting note: commented out locale
+open BigOperators
 
 variable {α : Type u} {β : Type v} {γ : Type w}
 

diff --git a/Mathlib/Algebra/BigOperators/RingEquiv.lean b/Mathlib/Algebra/BigOperators/RingEquiv.lean
@@ -18,8 +18,7 @@ import Mathlib.Algebra.Ring.Equiv
 
 namespace RingEquiv
 
--- Porting note : commented out the next line
--- open BigOperators
+open BigOperators
 
 variable {α R S : Type _}
 

diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean
@@ -27,8 +27,7 @@ This notation is in the `DirectSum` locale, accessible after `open_locale Direct
 * https://en.wikipedia.org/wiki/Direct_sum
 -/
 
--- Porting note: Unknown namespace
--- open BigOperators
+open BigOperators
 
 universe u v w u₁
 

diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean
@@ -40,8 +40,7 @@ variable {α : Type u}
 
 open Finset MulOpposite
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 section Semiring
 

diff --git a/Mathlib/Algebra/IndicatorFunction.lean b/Mathlib/Algebra/IndicatorFunction.lean
@@ -33,8 +33,7 @@ arguments. This is in contrast with the design of `Pi.Single` or `Set.Piecewise`
 indicator, characteristic
 -/
 
--- Porting note: unknown namespace BigOperators
--- open BigOperators
+open BigOperators
 
 open Function
 

diff --git a/Mathlib/Algebra/Module/BigOperators.lean b/Mathlib/Algebra/Module/BigOperators.lean
@@ -15,8 +15,7 @@ import Mathlib.GroupTheory.GroupAction.BigOperators
 # Finite sums over modules over a ring
 -/
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 variable {α β R M ι : Type _}
 

diff --git a/Mathlib/Algebra/Module/Submodule/Basic.lean b/Mathlib/Algebra/Module/Submodule/Basic.lean
@@ -32,7 +32,7 @@ submodule, subspace, linear map
 
 open Function
 
--- Porting note: notation is global open BigOperators
+open BigOperators
 
 universe u'' u' u v w
 

diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean
@@ -302,8 +302,7 @@ theorem mem_supᵢ_of_mem {ι : Sort _} {b : M} {p : ι → Submodule R M} (i :
   (le_supᵢ p i) h
 #align submodule.mem_supr_of_mem Submodule.mem_supᵢ_of_mem
 
--- Porting note: commented out
--- open BigOperators
+open BigOperators
 
 theorem sum_mem_supᵢ {ι : Type _} [Fintype ι] {f : ι → M} {p : ι → Submodule R M}
     (h : ∀ i, f i ∈ p i) : (∑ i, f i) ∈ ⨆ i, p i :=

diff --git a/Mathlib/Algebra/Star/BigOperators.lean b/Mathlib/Algebra/Star/BigOperators.lean
@@ -19,8 +19,7 @@ These results are kept separate from `Algebra.Star.Basic` to avoid it needing to
 
 variable {R : Type _}
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 @[simp]
 theorem star_prod [CommMonoid R] [StarSemigroup R] {α : Type _} (s : Finset α) (f : α → R) :

diff --git a/Mathlib/Algebra/Support.lean b/Mathlib/Algebra/Support.lean
@@ -26,8 +26,7 @@ We also define `Function.mulSupport f = {x | f x ≠ 1}`.
 
 open Set
 
---Porting note: namespace does not exist
---open BigOperators
+open BigOperators
 
 namespace Function
 

diff --git a/Mathlib/Algebra/Tropical/BigOperators.lean b/Mathlib/Algebra/Tropical/BigOperators.lean
@@ -36,8 +36,7 @@ directly transfer to minima over multisets or finsets.
 
 -/
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 variable {R S : Type _}
 

diff --git a/Mathlib/Combinatorics/DoubleCounting.lean b/Mathlib/Combinatorics/DoubleCounting.lean
@@ -34,8 +34,7 @@ and `t`.
 
 open Finset Function Relator
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 variable {α β : Type _}
 

diff --git a/Mathlib/Combinatorics/Pigeonhole.lean b/Mathlib/Combinatorics/Pigeonhole.lean
@@ -73,8 +73,7 @@ variable {α : Type u} {β : Type v} {M : Type w} [DecidableEq β]
 
 open Nat
 
--- porting note: The `BigOperators` notation is now global
--- open BigOperators
+open BigOperators
 
 namespace Finset
 

diff --git a/Mathlib/Data/Dfinsupp/Basic.lean b/Mathlib/Data/Dfinsupp/Basic.lean
@@ -51,7 +51,7 @@ definitions, or introduce two more definitions for the other combinations of dec
 
 universe u u₁ u₂ v v₁ v₂ v₃ w x y l
 
--- open BigOperators -- Porting note: notation is global for now
+open BigOperators
 
 variable {ι : Type u} {γ : Type w} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
 

diff --git a/Mathlib/Data/Fin/Interval.lean b/Mathlib/Data/Fin/Interval.lean
@@ -21,8 +21,7 @@ intervals as Finsets and Fintypes.
 
 open Finset Fin Function
 
--- Porting note: Uncomment once localised BigOperators is fixed:
--- open BigOperators
+open BigOperators
 
 variable (n : ℕ)
 

diff --git a/Mathlib/Data/Finset/LocallyFinite.lean b/Mathlib/Data/Finset/LocallyFinite.lean
@@ -31,9 +31,7 @@ for some ideas.
 
 open Function OrderDual
 
--- Porting note: Fix once big operators are localised again.
--- open BigOperators FinsetInterval
-open FinsetInterval
+open BigOperators FinsetInterval
 
 variable {ι α : Type _}
 

diff --git a/Mathlib/Data/Finset/Preimage.lean b/Mathlib/Data/Finset/Preimage.lean
@@ -18,7 +18,7 @@ import Mathlib.Algebra.BigOperators.Basic
 
 open Set Function
 
--- open BigOperators -- Porting note: notation is global for now
+open BigOperators
 
 universe u v w x
 

diff --git a/Mathlib/Data/Finset/Slice.lean b/Mathlib/Data/Finset/Slice.lean
@@ -34,7 +34,7 @@ the set family made of its `r`-sets.
 
 open Finset Nat
 
--- open BigOperators -- Porting note: commented out locale
+open BigOperators
 
 variable {α : Type _} {ι : Sort _} {κ : ι → Sort _}
 

diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean
@@ -88,7 +88,7 @@ noncomputable section
 
 open Finset Function
 
--- open BigOperators -- Porting note: notation is global for now
+open BigOperators
 
 variable {α β γ ι M M' N P G H R S : Type _}
 

diff --git a/Mathlib/Data/Finsupp/Order.lean b/Mathlib/Data/Finsupp/Order.lean
@@ -29,8 +29,7 @@ This file lifts order structures on `α` to `ι →₀ α`.
 
 noncomputable section
 
--- porting notes: not needed, doesn't exist
---open BigOperators
+open BigOperators
 
 open Finset
 

diff --git a/Mathlib/Data/Fintype/BigOperators.lean b/Mathlib/Data/Fintype/BigOperators.lean
@@ -34,7 +34,7 @@ universe u v
 
 variable {α : Type _} {β : Type _} {γ : Type _}
 
--- open BigOperators -- Porting note: notation is currently global
+open BigOperators
 
 namespace Fintype
 

diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean
@@ -23,7 +23,7 @@ While in terms of semantics they could be in the `Basic.lean` file, importing
 
 
 open Nat
--- Porting note: notation is currently global `open BigOperators`
+open BigOperators
 
 namespace Nat
 

diff --git a/Mathlib/Data/Nat/Fib.lean b/Mathlib/Data/Nat/Fib.lean
@@ -58,8 +58,7 @@ For efficiency purposes, the sequence is defined using `Stream.iterate`.
 fib, fibonacci
 -/
 
---Porting note: commented out
---open BigOperators
+open BigOperators
 
 namespace Nat
 

diff --git a/Mathlib/Data/Nat/GCD/BigOperators.lean b/Mathlib/Data/Nat/GCD/BigOperators.lean
@@ -19,8 +19,7 @@ These lemmas are kept separate from `Data.Nat.GCD.Basic` in order to minimize im
 
 namespace Nat
 
--- Porting note: commented out the next line
--- open BigOperators
+open BigOperators
 
 /-- See `IsCoprime.prod_left` for the corresponding lemma about `IsCoprime` -/
 theorem coprime_prod_left {ι : Type _} {x : ℕ} {s : ι → ℕ} {t : Finset ι} :

diff --git a/Mathlib/Data/Rat/BigOperators.lean b/Mathlib/Data/Rat/BigOperators.lean
@@ -14,8 +14,7 @@ import Mathlib.Algebra.BigOperators.Basic
 /-! # Casting lemmas for rational numbers involving sums and products
 -/
 
--- Porting note: big operators are currently global
---open BigOperators
+open BigOperators
 
 variable {ι α : Type _}
 

diff --git a/Mathlib/Data/Set/Equitable.lean b/Mathlib/Data/Set/Equitable.lean
@@ -26,7 +26,7 @@ latter yet.
 -/
 
 
--- Porting note: global for now: open BigOperators
+open BigOperators
 
 variable {α β : Type _}