Remove open BigOperators which does nothing

This used to be necessary, but the notation is available globally in recent mathlib versions.
trishullab · Oct 21, 2024 · cd7ff16 · cd7ff16
1 parent 258bbe8
commit cd7ff16
Show file tree

Hide file tree

Showing 641 changed files with 40 additions and 679 deletions.
diff --git a/lean4/scripts/generate_files_by_year.py b/lean4/scripts/generate_files_by_year.py
@@ -9,7 +9,7 @@ def all_to_years(min_year, max_year):
         for year in range(max_year, min_year - 1, -1):
             filename = f"putnam_{year}.lean"
             with open(filename, "w") as g:
-                g.write("import Mathlib\nopen BigOperators\n\n")
+                g.write("import Mathlib\n\n")
                 is_in_section = False
                 for line in lines:
                     if is_in_section:
@@ -21,14 +21,14 @@ def all_to_years(min_year, max_year):
 
 def years_to_all(min_year, max_year):
     with open("putnam_all.lean", "w") as f:
-        f.write("import Mathlib\nopen BigOperators\n\n")
+        f.write("import Mathlib\n\n")
         for year in range(min_year, max_year + 1):
             filename = f"putnam_{year}.lean"
             with open(filename, "r") as g:
                 lines = g.readlines()
                 f.write(f"section putnam_{year}\n")
                 for line in lines:
-                    if line.strip() == "import Mathlib" or line.strip() == "open BigOperators":
+                    if line.strip() == "import Mathlib":
                         continue
                     f.write(line)
                 f.write(f"end putnam_{year}\n")
@@ -45,7 +45,7 @@ def files_to_individual(min_year, max_year):
             problem_pattern = fr'putnam_{year}_[ab][1-6]'
 
             for idx, line in enumerate(lines):
-                if "Mathlib" in line or "BigOperators" in line:
+                if "Mathlib" in line:
                     continue
                 elif line.strip() == "" or idx == len(lines) - 1:
                     if idx == len(lines) - 1:
@@ -64,7 +64,7 @@ def files_to_individual(min_year, max_year):
                             print(f"Search is {search}")
                             assert False
                         with open(f"src/{problem_name}.lean", "w") as g:
-                            g.write("import Mathlib\nopen BigOperators\n\n")
+                            g.write("import Mathlib\n\n")
                             if len(running_scopes) > 0:
                                 g.write(f"open {' '.join(running_scopes)}\n\n")
                             for line in section_content:
@@ -106,7 +106,7 @@ def all_to_individual(min_year, max_year):
 
                     filename = f"putnam_{section_name}.lean"
                     with open(filename, "w") as g:
-                        g.write("import Mathlib\nopen BigOperators\n")
+                        g.write("import Mathlib\n")
                         for namespace in namespaces:
                             g.write(f"open {namespace}\n")
                         g.write("\n")

diff --git a/lean4/src/putnam_1962_a1.lean b/lean4/src/putnam_1962_a1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open MeasureTheory
 

diff --git a/lean4/src/putnam_1962_a2.lean b/lean4/src/putnam_1962_a2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open MeasureTheory Set
 

diff --git a/lean4/src/putnam_1962_a3.lean b/lean4/src/putnam_1962_a3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open MeasureTheory
 

diff --git a/lean4/src/putnam_1962_a4.lean b/lean4/src/putnam_1962_a4.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 /--
 Assume that $\lvert f(x) \rvert \le 1$ and $\lvert f''(x) \rvert \le 1$ for all $x$ on an interval of length at least 2. Show that $\lvert f'(x) \rvert \le 2$ on the interval.

diff --git a/lean4/src/putnam_1962_a5.lean b/lean4/src/putnam_1962_a5.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 abbrev putnam_1962_a5_solution : ℕ → ℕ := sorry
 -- fun n : ℕ => n * (n + 1) * 2^(n - 2)

diff --git a/lean4/src/putnam_1962_a6.lean b/lean4/src/putnam_1962_a6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 /--
 Let $S$ be a set of rational numbers such that whenever $a$ and $b$ are members of $S$, so are $a+b$ and $ab$, and having the property that for every rational number $r$ exactly one of the following three statements is true: \[ r \in S, -r \in S, r = 0. \] Prove that $S$ is the set of all positive rational numbers.

diff --git a/lean4/src/putnam_1962_b1.lean b/lean4/src/putnam_1962_b1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 /--
 Let $x^{(n)} = x(x-1)\cdots(x-n+1)$ for $n$ a positive integer and let $x^{(0)} = 1.$ Prove that \[ (x+y)^{(n)} = \sum_{k=0}^n {n \choose k} x^{(k)} y^{(n-k)}. \]

diff --git a/lean4/src/putnam_1962_b2.lean b/lean4/src/putnam_1962_b2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open MeasureTheory
 

diff --git a/lean4/src/putnam_1962_b3.lean b/lean4/src/putnam_1962_b3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open MeasureTheory
 

diff --git a/lean4/src/putnam_1962_b5.lean b/lean4/src/putnam_1962_b5.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open MeasureTheory
 

diff --git a/lean4/src/putnam_1962_b6.lean b/lean4/src/putnam_1962_b6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Real
 

diff --git a/lean4/src/putnam_1963_a2.lean b/lean4/src/putnam_1963_a2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter
 

diff --git a/lean4/src/putnam_1963_a3.lean b/lean4/src/putnam_1963_a3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Nat Set Topology Filter
 

diff --git a/lean4/src/putnam_1963_a4.lean b/lean4/src/putnam_1963_a4.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Filter Set
 

diff --git a/lean4/src/putnam_1963_a6.lean b/lean4/src/putnam_1963_a6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter
 

diff --git a/lean4/src/putnam_1963_b1.lean b/lean4/src/putnam_1963_b1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter Polynomial
 

diff --git a/lean4/src/putnam_1963_b2.lean b/lean4/src/putnam_1963_b2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter Polynomial
 

diff --git a/lean4/src/putnam_1963_b3.lean b/lean4/src/putnam_1963_b3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter Polynomial
 

diff --git a/lean4/src/putnam_1963_b5.lean b/lean4/src/putnam_1963_b5.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter Polynomial
 

diff --git a/lean4/src/putnam_1963_b6.lean b/lean4/src/putnam_1963_b6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter Polynomial
 

diff --git a/lean4/src/putnam_1964_a1.lean b/lean4/src/putnam_1964_a1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 /--
 Let $A_1, A_2, A_3, A_4, A_5, A_6$ be distinct points in the plane. Let $D$ be the longest distance between any pair, and let $d$ the shortest distance. Show that $\frac{D}{d} \geq \sqrt 3$.

diff --git a/lean4/src/putnam_1964_a2.lean b/lean4/src/putnam_1964_a2.lean
@@ -1,13 +1,12 @@
 import Mathlib
-open BigOperators
 
 open Set
 
 -- Note: uses (ℝ → ℝ) instead of (Icc 0 1 → ℝ)
 abbrev putnam_1964_a2_solution : ℝ → Set (ℝ → ℝ) := sorry
 -- fun _ ↦ ∅
 /--
-Let $\alpha$ be a real number. Find all continuous real-valued functions $f : [0, 1] \to (0, \infty)$ such that 
+Let $\alpha$ be a real number. Find all continuous real-valued functions $f : [0, 1] \to (0, \infty)$ such that
 \begin{align*}
 \int_0^1 f(x) dx &= 1, \\
 \int_0^1 x f(x) dx &= \alpha, \\

diff --git a/lean4/src/putnam_1964_a3.lean b/lean4/src/putnam_1964_a3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Set Function
 

diff --git a/lean4/src/putnam_1964_a4.lean b/lean4/src/putnam_1964_a4.lean
@@ -1,13 +1,12 @@
 import Mathlib
-open BigOperators
 
 open Set Function
 
 /--
-The sequence of integers $u_n$ is bounded and satisfies 
+The sequence of integers $u_n$ is bounded and satisfies
 \[
 u_n = \frac{u_{n-1} + u_{n-2} + u_{n-3}u_{n-4}}{u_{n-1}u_{n-2} + u_{n-3} + u_{n-4}}.
-\] 
+\]
 Show that it is periodic for sufficiently large $n$.
 -/
 theorem putnam_1964_a4

diff --git a/lean4/src/putnam_1964_a5.lean b/lean4/src/putnam_1964_a5.lean
@@ -1,10 +1,9 @@
 import Mathlib
-open BigOperators
 
 open Set Function Filter Topology
 
 /--
-Prove that there exists a constant $k$ such that for any sequence $a_i$ of positive numbers, 
+Prove that there exists a constant $k$ such that for any sequence $a_i$ of positive numbers,
 \[
 \sum_{n=1}^{\infty} \frac{n}{a_1 + a_2 + \dots + a_n} \leq k \sum_{n=1}^{\infty}\frac{1}{a_n}.
 \]

diff --git a/lean4/src/putnam_1964_a6.lean b/lean4/src/putnam_1964_a6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Set Function Filter Topology
 

diff --git a/lean4/src/putnam_1964_b1.lean b/lean4/src/putnam_1964_b1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Set Function Filter Topology
 

diff --git a/lean4/src/putnam_1964_b2.lean b/lean4/src/putnam_1964_b2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Set Function Filter Topology
 

diff --git a/lean4/src/putnam_1964_b3.lean b/lean4/src/putnam_1964_b3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Set Function Filter Topology
 

diff --git a/lean4/src/putnam_1964_b5.lean b/lean4/src/putnam_1964_b5.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Set Function Filter Topology
 

diff --git a/lean4/src/putnam_1964_b6.lean b/lean4/src/putnam_1964_b6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Set Function Filter Topology
 

diff --git a/lean4/src/putnam_1965_a1.lean b/lean4/src/putnam_1965_a1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Real
 

diff --git a/lean4/src/putnam_1965_a2.lean b/lean4/src/putnam_1965_a2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry
 

diff --git a/lean4/src/putnam_1965_a3.lean b/lean4/src/putnam_1965_a3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_a4.lean b/lean4/src/putnam_1965_a4.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_a5.lean b/lean4/src/putnam_1965_a5.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_a6.lean b/lean4/src/putnam_1965_a6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_b1.lean b/lean4/src/putnam_1965_b1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_b2.lean b/lean4/src/putnam_1965_b2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_b3.lean b/lean4/src/putnam_1965_b3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_b4.lean b/lean4/src/putnam_1965_b4.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex
 

diff --git a/lean4/src/putnam_1965_b5.lean b/lean4/src/putnam_1965_b5.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk
 

diff --git a/lean4/src/putnam_1965_b6.lean b/lean4/src/putnam_1965_b6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open EuclideanGeometry Topology Filter Complex SimpleGraph.Walk
 

diff --git a/lean4/src/putnam_1966_a1.lean b/lean4/src/putnam_1966_a1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 /--
 Let $a_n$ denote the sequence $0, 1, 1, 2, 2, 3, \dots$, where $a_n = \frac{n}{2}$ if $n$ is even and $\frac{n - 1}{2}$ if n is odd. Furthermore, let $f(n)$ denote the sum of the first $n$ terms of $a_n$. Prove that all positive integers $x$ and $y$ with $x > y$ satisfy $xy = f(x + y) - f(x - y)$.

diff --git a/lean4/src/putnam_1966_a2.lean b/lean4/src/putnam_1966_a2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 /--
 Let $a$, $b$, and $c$ be the side lengths of a triangle with inradius $r$. If $p = \frac{a + b + c}{2}$, show that $$\frac{1}{(p - a)^2} + \frac{1}{(p - b)^2} + \frac{1}{(p - c)^2} \ge \frac{1}{r^2}.$$

diff --git a/lean4/src/putnam_1966_a3.lean b/lean4/src/putnam_1966_a3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter
 

diff --git a/lean4/src/putnam_1966_a4.lean b/lean4/src/putnam_1966_a4.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter
 

diff --git a/lean4/src/putnam_1966_a5.lean b/lean4/src/putnam_1966_a5.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter
 

diff --git a/lean4/src/putnam_1966_a6.lean b/lean4/src/putnam_1966_a6.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter
 

diff --git a/lean4/src/putnam_1966_b1.lean b/lean4/src/putnam_1966_b1.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology
 

diff --git a/lean4/src/putnam_1966_b2.lean b/lean4/src/putnam_1966_b2.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 /--
 Prove that, for any ten consecutive integers, at least one is relatively prime to all of the others.

diff --git a/lean4/src/putnam_1966_b3.lean b/lean4/src/putnam_1966_b3.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter
 

diff --git a/lean4/src/putnam_1966_b4.lean b/lean4/src/putnam_1966_b4.lean
@@ -1,5 +1,4 @@
 import Mathlib
-open BigOperators
 
 open Topology Filter