diff --git a/lean4/scripts/generate_files_by_year.py b/lean4/scripts/generate_files_by_year.py index 8964d715..018cdba6 100644 --- 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 index 9f1422a9..bc940d02 100644 --- 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 index 9dcf7d14..10c21fdf 100644 --- 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 index 50360174..25d3fb29 100644 --- 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 index fc896b85..01062553 100644 --- 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 index 208b6645..a9e93cad 100644 --- 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 index a7d202b9..b81a91f2 100644 --- 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 index 8e0a9f59..6a8d1d7e 100644 --- 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 index 8cb176d5..e80d088b 100644 --- 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 index 5267fb17..36c96b74 100644 --- 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 index c9d62344..9477f53b 100644 --- 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 index 9e214d01..988cd188 100644 --- 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 index 66f14c7c..76b01060 100644 --- 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 index c357462e..cfaca34a 100644 --- 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 index 803a5988..c7b09311 100644 --- 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 index 1df44be7..7add62d5 100644 --- 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 index 48d4a770..f14b9195 100644 --- 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 index 261d941a..65d56a6a 100644 --- 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 index aaff0c28..69511d4c 100644 --- 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 index 454f9b78..c2752d8d 100644 --- 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 index fef2505e..8e4b66c3 100644 --- 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 index 0b611690..24049c13 100644 --- 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 index 3390dbde..ac8fa052 100644 --- a/lean4/src/putnam_1964_a2.lean +++ b/lean4/src/putnam_1964_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1964_a3.lean b/lean4/src/putnam_1964_a3.lean index 455608f4..594528d9 100644 --- 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 index 07a68f4a..70bb33a2 100644 --- a/lean4/src/putnam_1964_a4.lean +++ b/lean4/src/putnam_1964_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function diff --git a/lean4/src/putnam_1964_a5.lean b/lean4/src/putnam_1964_a5.lean index 36ef8031..afd583e9 100644 --- a/lean4/src/putnam_1964_a5.lean +++ b/lean4/src/putnam_1964_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology diff --git a/lean4/src/putnam_1964_a6.lean b/lean4/src/putnam_1964_a6.lean index c7a1f6f9..453fb76d 100644 --- 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 index 05320397..24d50230 100644 --- 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 index 382d3443..9d7e6728 100644 --- 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 index 78b1aed6..147fdbba 100644 --- 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 index dee633ba..72643cc8 100644 --- 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 index cbe0818d..32f70a51 100644 --- 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 index 4b71b3c1..2b2a17c1 100644 --- 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 index 6149cb72..9fbe1c42 100644 --- 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 index 3521325b..7e269db2 100644 --- 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 index f5425598..b6937ac5 100644 --- 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 index 6c99a86c..940ae757 100644 --- 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 index e62ec376..280095bb 100644 --- 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 index 019576be..0179e3d1 100644 --- 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 index f6254d44..eb8b2e24 100644 --- 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 index d497269e..649637d7 100644 --- 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 index ee3c8127..e2d2bf25 100644 --- 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 index 80c60180..ddc133f4 100644 --- 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 index ea6c9ba4..4a9ababd 100644 --- 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 index f9846bd6..d59fdc6e 100644 --- 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 index 03406044..12928635 100644 --- 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 index c0fd9d94..8c393150 100644 --- 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 index 275227d8..acbfd7dc 100644 --- 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 index 2ac53676..cc183f3e 100644 --- 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 index 07c1df0c..a4ff0eb1 100644 --- 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 index 5b2472a5..b4b8bcf3 100644 --- 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 index a5c7c6eb..9de34735 100644 --- 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 index 967a1273..1444f013 100644 --- 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 index 848f6209..c2d3dd0a 100644 --- 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 diff --git a/lean4/src/putnam_1966_b5.lean b/lean4/src/putnam_1966_b5.lean index 7144cdbf..ae0894e4 100644 --- a/lean4/src/putnam_1966_b5.lean +++ b/lean4/src/putnam_1966_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_1966_b6.lean b/lean4/src/putnam_1966_b6.lean index b5bbaea1..809291a5 100644 --- a/lean4/src/putnam_1966_b6.lean +++ b/lean4/src/putnam_1966_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_1967_a1.lean b/lean4/src/putnam_1967_a1.lean index 517420aa..66e062e7 100644 --- a/lean4/src/putnam_1967_a1.lean +++ b/lean4/src/putnam_1967_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_a2.lean b/lean4/src/putnam_1967_a2.lean index 4b6edb43..f62f4efe 100644 --- a/lean4/src/putnam_1967_a2.lean +++ b/lean4/src/putnam_1967_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_a3.lean b/lean4/src/putnam_1967_a3.lean index de3a86d6..cc303183 100644 --- a/lean4/src/putnam_1967_a3.lean +++ b/lean4/src/putnam_1967_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_a4.lean b/lean4/src/putnam_1967_a4.lean index 555c7522..7e46b52b 100644 --- a/lean4/src/putnam_1967_a4.lean +++ b/lean4/src/putnam_1967_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_a5.lean b/lean4/src/putnam_1967_a5.lean index 37a64284..f3baf2a6 100644 --- a/lean4/src/putnam_1967_a5.lean +++ b/lean4/src/putnam_1967_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_a6.lean b/lean4/src/putnam_1967_a6.lean index ce8f1649..f462b89d 100644 --- a/lean4/src/putnam_1967_a6.lean +++ b/lean4/src/putnam_1967_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_b1.lean b/lean4/src/putnam_1967_b1.lean index cc904c09..c4404d18 100644 --- a/lean4/src/putnam_1967_b1.lean +++ b/lean4/src/putnam_1967_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_b2.lean b/lean4/src/putnam_1967_b2.lean index b73bb97c..6dfdc20e 100644 --- a/lean4/src/putnam_1967_b2.lean +++ b/lean4/src/putnam_1967_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_b3.lean b/lean4/src/putnam_1967_b3.lean index 15effa7d..4d091d16 100644 --- a/lean4/src/putnam_1967_b3.lean +++ b/lean4/src/putnam_1967_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_b4.lean b/lean4/src/putnam_1967_b4.lean index 4cb236dd..633b08ac 100644 --- a/lean4/src/putnam_1967_b4.lean +++ b/lean4/src/putnam_1967_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_b5.lean b/lean4/src/putnam_1967_b5.lean index 5896d2c9..58cc6c9c 100644 --- a/lean4/src/putnam_1967_b5.lean +++ b/lean4/src/putnam_1967_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1967_b6.lean b/lean4/src/putnam_1967_b6.lean index 577da971..b5bf530d 100644 --- a/lean4/src/putnam_1967_b6.lean +++ b/lean4/src/putnam_1967_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_1968_a1.lean b/lean4/src/putnam_1968_a1.lean index 97f9a9b9..bc3d519b 100644 --- a/lean4/src/putnam_1968_a1.lean +++ b/lean4/src/putnam_1968_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Prove that $$\frac{22}{7} - \pi = \int_{0}^{1} \frac{x^4(1 - x)^4}{1 + x^2} dx$$. diff --git a/lean4/src/putnam_1968_a2.lean b/lean4/src/putnam_1968_a2.lean index b3d0b8d4..02a1162a 100644 --- a/lean4/src/putnam_1968_a2.lean +++ b/lean4/src/putnam_1968_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- For all integers $a$, $b$, $c$, $d$, $e$, and $f$ such that $ad \neq bc$ and any real number $\epsilon > 0$, prove that there exist rational numbers $r$ and $s$ such that $$0 < |ra + sb - e| < \varepsilon$$ and $$0 < |rc + sd - f| < \varepsilon.$$ diff --git a/lean4/src/putnam_1968_a3.lean b/lean4/src/putnam_1968_a3.lean index 6a49bf10..ff32f1a1 100644 --- a/lean4/src/putnam_1968_a3.lean +++ b/lean4/src/putnam_1968_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset symmDiff diff --git a/lean4/src/putnam_1968_a4.lean b/lean4/src/putnam_1968_a4.lean index 05bb6316..c5e83c3d 100644 --- a/lean4/src/putnam_1968_a4.lean +++ b/lean4/src/putnam_1968_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset diff --git a/lean4/src/putnam_1968_a5.lean b/lean4/src/putnam_1968_a5.lean index 44be2758..507ee5ed 100644 --- a/lean4/src/putnam_1968_a5.lean +++ b/lean4/src/putnam_1968_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset Polynomial diff --git a/lean4/src/putnam_1968_a6.lean b/lean4/src/putnam_1968_a6.lean index b38de6b6..301a23e6 100644 --- a/lean4/src/putnam_1968_a6.lean +++ b/lean4/src/putnam_1968_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset Polynomial diff --git a/lean4/src/putnam_1968_b2.lean b/lean4/src/putnam_1968_b2.lean index 1f5ea47e..feabce14 100644 --- a/lean4/src/putnam_1968_b2.lean +++ b/lean4/src/putnam_1968_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset Polynomial diff --git a/lean4/src/putnam_1968_b4.lean b/lean4/src/putnam_1968_b4.lean index bc0f2f5f..473030da 100644 --- a/lean4/src/putnam_1968_b4.lean +++ b/lean4/src/putnam_1968_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset Polynomial Topology Filter Metric diff --git a/lean4/src/putnam_1968_b5.lean b/lean4/src/putnam_1968_b5.lean index b331097b..53d7240d 100644 --- a/lean4/src/putnam_1968_b5.lean +++ b/lean4/src/putnam_1968_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset Polynomial Topology Filter Metric diff --git a/lean4/src/putnam_1968_b6.lean b/lean4/src/putnam_1968_b6.lean index e9d47d68..f3069eaa 100644 --- a/lean4/src/putnam_1968_b6.lean +++ b/lean4/src/putnam_1968_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Finset Polynomial Topology Filter Metric diff --git a/lean4/src/putnam_1969_a1.lean b/lean4/src/putnam_1969_a1.lean index 90e92389..b1391f14 100644 --- a/lean4/src/putnam_1969_a1.lean +++ b/lean4/src/putnam_1969_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_a2.lean b/lean4/src/putnam_1969_a2.lean index b775130a..2f39d4a8 100644 --- a/lean4/src/putnam_1969_a2.lean +++ b/lean4/src/putnam_1969_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_a4.lean b/lean4/src/putnam_1969_a4.lean index f1e8416b..02d764e6 100644 --- a/lean4/src/putnam_1969_a4.lean +++ b/lean4/src/putnam_1969_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_a5.lean b/lean4/src/putnam_1969_a5.lean index 2de76cc3..30935e05 100644 --- a/lean4/src/putnam_1969_a5.lean +++ b/lean4/src/putnam_1969_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_a6.lean b/lean4/src/putnam_1969_a6.lean index 4dfefcb6..b0ccd2a8 100644 --- a/lean4/src/putnam_1969_a6.lean +++ b/lean4/src/putnam_1969_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_b1.lean b/lean4/src/putnam_1969_b1.lean index 89e65d13..1e17dd30 100644 --- a/lean4/src/putnam_1969_b1.lean +++ b/lean4/src/putnam_1969_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_b2.lean b/lean4/src/putnam_1969_b2.lean index b680db96..c68d31b9 100644 --- a/lean4/src/putnam_1969_b2.lean +++ b/lean4/src/putnam_1969_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_b3.lean b/lean4/src/putnam_1969_b3.lean index 5a86acda..9c9b2e6c 100644 --- a/lean4/src/putnam_1969_b3.lean +++ b/lean4/src/putnam_1969_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_b5.lean b/lean4/src/putnam_1969_b5.lean index e1a67b0f..d0d02c97 100644 --- a/lean4/src/putnam_1969_b5.lean +++ b/lean4/src/putnam_1969_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1969_b6.lean b/lean4/src/putnam_1969_b6.lean index 88c20625..5b9ff5ec 100644 --- a/lean4/src/putnam_1969_b6.lean +++ b/lean4/src/putnam_1969_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Filter Topology Set Nat diff --git a/lean4/src/putnam_1970_a1.lean b/lean4/src/putnam_1970_a1.lean index f68fed85..94f7a85d 100644 --- a/lean4/src/putnam_1970_a1.lean +++ b/lean4/src/putnam_1970_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry diff --git a/lean4/src/putnam_1970_a2.lean b/lean4/src/putnam_1970_a2.lean index 5ebb64ad..59466496 100644 --- a/lean4/src/putnam_1970_a2.lean +++ b/lean4/src/putnam_1970_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry diff --git a/lean4/src/putnam_1970_a3.lean b/lean4/src/putnam_1970_a3.lean index ce0848ad..a9ec50b1 100644 --- a/lean4/src/putnam_1970_a3.lean +++ b/lean4/src/putnam_1970_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry diff --git a/lean4/src/putnam_1970_a4.lean b/lean4/src/putnam_1970_a4.lean index 3366c42f..4a68a3c8 100644 --- a/lean4/src/putnam_1970_a4.lean +++ b/lean4/src/putnam_1970_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry Filter Topology diff --git a/lean4/src/putnam_1970_b1.lean b/lean4/src/putnam_1970_b1.lean index 1542189a..86c12734 100644 --- a/lean4/src/putnam_1970_b1.lean +++ b/lean4/src/putnam_1970_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry Filter Topology diff --git a/lean4/src/putnam_1970_b2.lean b/lean4/src/putnam_1970_b2.lean index f7ba0b84..3070a461 100644 --- a/lean4/src/putnam_1970_b2.lean +++ b/lean4/src/putnam_1970_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry Filter Topology diff --git a/lean4/src/putnam_1970_b3.lean b/lean4/src/putnam_1970_b3.lean index 95d2933e..ca3f7cde 100644 --- a/lean4/src/putnam_1970_b3.lean +++ b/lean4/src/putnam_1970_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry Filter Topology diff --git a/lean4/src/putnam_1970_b4.lean b/lean4/src/putnam_1970_b4.lean index 9179a06c..1a1880a6 100644 --- a/lean4/src/putnam_1970_b4.lean +++ b/lean4/src/putnam_1970_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry Filter Topology diff --git a/lean4/src/putnam_1970_b5.lean b/lean4/src/putnam_1970_b5.lean index 03c73f06..c8771863 100644 --- a/lean4/src/putnam_1970_b5.lean +++ b/lean4/src/putnam_1970_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry Filter Topology diff --git a/lean4/src/putnam_1970_b6.lean b/lean4/src/putnam_1970_b6.lean index e103967e..e809431e 100644 --- a/lean4/src/putnam_1970_b6.lean +++ b/lean4/src/putnam_1970_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric Set EuclideanGeometry Filter Topology diff --git a/lean4/src/putnam_1971_a1.lean b/lean4/src/putnam_1971_a1.lean index 6afe95ca..1ec7ad47 100644 --- a/lean4/src/putnam_1971_a1.lean +++ b/lean4/src/putnam_1971_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1971_a2.lean b/lean4/src/putnam_1971_a2.lean index b535e696..6aa00afe 100644 --- a/lean4/src/putnam_1971_a2.lean +++ b/lean4/src/putnam_1971_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1971_a3.lean b/lean4/src/putnam_1971_a3.lean index 19f26ef5..0b0f0a87 100644 --- a/lean4/src/putnam_1971_a3.lean +++ b/lean4/src/putnam_1971_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1971_a4.lean b/lean4/src/putnam_1971_a4.lean index 8a2ecb40..e307bd9a 100644 --- a/lean4/src/putnam_1971_a4.lean +++ b/lean4/src/putnam_1971_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set MvPolynomial diff --git a/lean4/src/putnam_1971_a5.lean b/lean4/src/putnam_1971_a5.lean index 2ceaa815..a134900e 100644 --- a/lean4/src/putnam_1971_a5.lean +++ b/lean4/src/putnam_1971_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set MvPolynomial diff --git a/lean4/src/putnam_1971_a6.lean b/lean4/src/putnam_1971_a6.lean index e27c03e5..e544d2b7 100644 --- a/lean4/src/putnam_1971_a6.lean +++ b/lean4/src/putnam_1971_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set MvPolynomial diff --git a/lean4/src/putnam_1971_b1.lean b/lean4/src/putnam_1971_b1.lean index 038eea5c..27d10d11 100644 --- a/lean4/src/putnam_1971_b1.lean +++ b/lean4/src/putnam_1971_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set MvPolynomial diff --git a/lean4/src/putnam_1971_b2.lean b/lean4/src/putnam_1971_b2.lean index 1e1a1fa0..1f68b935 100644 --- a/lean4/src/putnam_1971_b2.lean +++ b/lean4/src/putnam_1971_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set MvPolynomial diff --git a/lean4/src/putnam_1971_b3.lean b/lean4/src/putnam_1971_b3.lean index 8d6ce245..0265166d 100644 --- a/lean4/src/putnam_1971_b3.lean +++ b/lean4/src/putnam_1971_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set MvPolynomial diff --git a/lean4/src/putnam_1971_b6.lean b/lean4/src/putnam_1971_b6.lean index 3a7bdf74..6b8494dc 100644 --- a/lean4/src/putnam_1971_b6.lean +++ b/lean4/src/putnam_1971_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set MvPolynomial diff --git a/lean4/src/putnam_1972_a1.lean b/lean4/src/putnam_1972_a1.lean index c94278c5..7d4ffdf0 100644 --- a/lean4/src/putnam_1972_a1.lean +++ b/lean4/src/putnam_1972_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set diff --git a/lean4/src/putnam_1972_a2.lean b/lean4/src/putnam_1972_a2.lean index 5e7d1242..aa6ca852 100644 --- a/lean4/src/putnam_1972_a2.lean +++ b/lean4/src/putnam_1972_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set diff --git a/lean4/src/putnam_1972_a3.lean b/lean4/src/putnam_1972_a3.lean index 1240ae33..cac34689 100644 --- a/lean4/src/putnam_1972_a3.lean +++ b/lean4/src/putnam_1972_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set diff --git a/lean4/src/putnam_1972_a5.lean b/lean4/src/putnam_1972_a5.lean index b737445b..affd7302 100644 --- a/lean4/src/putnam_1972_a5.lean +++ b/lean4/src/putnam_1972_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set diff --git a/lean4/src/putnam_1972_a6.lean b/lean4/src/putnam_1972_a6.lean index bae8a91c..ffa3cb37 100644 --- a/lean4/src/putnam_1972_a6.lean +++ b/lean4/src/putnam_1972_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set MeasureTheory diff --git a/lean4/src/putnam_1972_b1.lean b/lean4/src/putnam_1972_b1.lean index c963cf28..663b5533 100644 --- a/lean4/src/putnam_1972_b1.lean +++ b/lean4/src/putnam_1972_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set MeasureTheory Metric diff --git a/lean4/src/putnam_1972_b2.lean b/lean4/src/putnam_1972_b2.lean index f14c3795..f5cbab9b 100644 --- a/lean4/src/putnam_1972_b2.lean +++ b/lean4/src/putnam_1972_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set MeasureTheory Metric diff --git a/lean4/src/putnam_1972_b3.lean b/lean4/src/putnam_1972_b3.lean index be89ef30..687bcac5 100644 --- a/lean4/src/putnam_1972_b3.lean +++ b/lean4/src/putnam_1972_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set MeasureTheory Metric diff --git a/lean4/src/putnam_1972_b4.lean b/lean4/src/putnam_1972_b4.lean index fa481550..45271c04 100644 --- a/lean4/src/putnam_1972_b4.lean +++ b/lean4/src/putnam_1972_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set MeasureTheory Metric diff --git a/lean4/src/putnam_1972_b5.lean b/lean4/src/putnam_1972_b5.lean index 95d33ab1..a7e291be 100644 --- a/lean4/src/putnam_1972_b5.lean +++ b/lean4/src/putnam_1972_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Set Metric diff --git a/lean4/src/putnam_1972_b6.lean b/lean4/src/putnam_1972_b6.lean index fe55178b..ad982dad 100644 --- a/lean4/src/putnam_1972_b6.lean +++ b/lean4/src/putnam_1972_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open EuclideanGeometry Filter Topology Set MeasureTheory Metric diff --git a/lean4/src/putnam_1973_a1.lean b/lean4/src/putnam_1973_a1.lean index f6668422..287c91fc 100644 --- a/lean4/src/putnam_1973_a1.lean +++ b/lean4/src/putnam_1973_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_a2.lean b/lean4/src/putnam_1973_a2.lean index d0c09594..e03d8211 100644 --- a/lean4/src/putnam_1973_a2.lean +++ b/lean4/src/putnam_1973_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_a3.lean b/lean4/src/putnam_1973_a3.lean index 1cc796eb..3d14eda2 100644 --- a/lean4/src/putnam_1973_a3.lean +++ b/lean4/src/putnam_1973_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_a4.lean b/lean4/src/putnam_1973_a4.lean index 9a912142..16ccf3b7 100644 --- a/lean4/src/putnam_1973_a4.lean +++ b/lean4/src/putnam_1973_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_a6.lean b/lean4/src/putnam_1973_a6.lean index 6e0b4a3e..6e110774 100644 --- a/lean4/src/putnam_1973_a6.lean +++ b/lean4/src/putnam_1973_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_b1.lean b/lean4/src/putnam_1973_b1.lean index b836219e..0075ca5e 100644 --- a/lean4/src/putnam_1973_b1.lean +++ b/lean4/src/putnam_1973_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_b2.lean b/lean4/src/putnam_1973_b2.lean index 76004038..50128357 100644 --- a/lean4/src/putnam_1973_b2.lean +++ b/lean4/src/putnam_1973_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_b3.lean b/lean4/src/putnam_1973_b3.lean index 504dd8fa..14008520 100644 --- a/lean4/src/putnam_1973_b3.lean +++ b/lean4/src/putnam_1973_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1973_b4.lean b/lean4/src/putnam_1973_b4.lean index fee71a9d..f1a1707b 100644 --- a/lean4/src/putnam_1973_b4.lean +++ b/lean4/src/putnam_1973_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set MeasureTheory Topology Filter diff --git a/lean4/src/putnam_1974_a1.lean b/lean4/src/putnam_1974_a1.lean index 0ada9a96..e685ac6c 100644 --- a/lean4/src/putnam_1974_a1.lean +++ b/lean4/src/putnam_1974_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1974_a3.lean b/lean4/src/putnam_1974_a3.lean index 59441b7d..d3a679a1 100644 --- a/lean4/src/putnam_1974_a3.lean +++ b/lean4/src/putnam_1974_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1974_a4.lean b/lean4/src/putnam_1974_a4.lean index 6c11f085..6e90e164 100644 --- a/lean4/src/putnam_1974_a4.lean +++ b/lean4/src/putnam_1974_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat diff --git a/lean4/src/putnam_1974_a6.lean b/lean4/src/putnam_1974_a6.lean index a0f29114..a4bcd1b6 100644 --- a/lean4/src/putnam_1974_a6.lean +++ b/lean4/src/putnam_1974_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Polynomial diff --git a/lean4/src/putnam_1974_b1.lean b/lean4/src/putnam_1974_b1.lean index 10563ee0..10499aa7 100644 --- a/lean4/src/putnam_1974_b1.lean +++ b/lean4/src/putnam_1974_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Polynomial diff --git a/lean4/src/putnam_1974_b2.lean b/lean4/src/putnam_1974_b2.lean index 4f99327f..90d37f8e 100644 --- a/lean4/src/putnam_1974_b2.lean +++ b/lean4/src/putnam_1974_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Polynomial Filter Topology diff --git a/lean4/src/putnam_1974_b3.lean b/lean4/src/putnam_1974_b3.lean index d394c747..02c5d89c 100644 --- a/lean4/src/putnam_1974_b3.lean +++ b/lean4/src/putnam_1974_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Polynomial Filter Topology diff --git a/lean4/src/putnam_1974_b4.lean b/lean4/src/putnam_1974_b4.lean index 49fdecd6..14864f54 100644 --- a/lean4/src/putnam_1974_b4.lean +++ b/lean4/src/putnam_1974_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Polynomial Filter Topology diff --git a/lean4/src/putnam_1974_b5.lean b/lean4/src/putnam_1974_b5.lean index 3e2bf12a..1187a296 100644 --- a/lean4/src/putnam_1974_b5.lean +++ b/lean4/src/putnam_1974_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Polynomial Filter Topology diff --git a/lean4/src/putnam_1974_b6.lean b/lean4/src/putnam_1974_b6.lean index ffb0f1e7..1747942d 100644 --- a/lean4/src/putnam_1974_b6.lean +++ b/lean4/src/putnam_1974_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Polynomial Filter Topology diff --git a/lean4/src/putnam_1975_a1.lean b/lean4/src/putnam_1975_a1.lean index 28d3b90e..382ead63 100644 --- a/lean4/src/putnam_1975_a1.lean +++ b/lean4/src/putnam_1975_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_1975_a2.lean b/lean4/src/putnam_1975_a2.lean index d2f53c83..9723066e 100644 --- a/lean4/src/putnam_1975_a2.lean +++ b/lean4/src/putnam_1975_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_1975_a3.lean b/lean4/src/putnam_1975_a3.lean index 93ec6a9c..3d3d634b 100644 --- a/lean4/src/putnam_1975_a3.lean +++ b/lean4/src/putnam_1975_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_1975_a4.lean b/lean4/src/putnam_1975_a4.lean index 57438983..bbd82d1b 100644 --- a/lean4/src/putnam_1975_a4.lean +++ b/lean4/src/putnam_1975_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex diff --git a/lean4/src/putnam_1975_a5.lean b/lean4/src/putnam_1975_a5.lean index bd58d996..b7736eda 100644 --- a/lean4/src/putnam_1975_a5.lean +++ b/lean4/src/putnam_1975_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex diff --git a/lean4/src/putnam_1975_b1.lean b/lean4/src/putnam_1975_b1.lean index 0a0e4dd0..b8803057 100644 --- a/lean4/src/putnam_1975_b1.lean +++ b/lean4/src/putnam_1975_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex diff --git a/lean4/src/putnam_1975_b2.lean b/lean4/src/putnam_1975_b2.lean index 50d087d8..0c0c9d83 100644 --- a/lean4/src/putnam_1975_b2.lean +++ b/lean4/src/putnam_1975_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex Matrix Filter Topology diff --git a/lean4/src/putnam_1975_b3.lean b/lean4/src/putnam_1975_b3.lean index e3c4a402..476618b6 100644 --- a/lean4/src/putnam_1975_b3.lean +++ b/lean4/src/putnam_1975_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex Matrix Filter Topology Multiset diff --git a/lean4/src/putnam_1975_b4.lean b/lean4/src/putnam_1975_b4.lean index 878d714e..4f37d12d 100644 --- a/lean4/src/putnam_1975_b4.lean +++ b/lean4/src/putnam_1975_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex Matrix Filter Topology Multiset diff --git a/lean4/src/putnam_1975_b5.lean b/lean4/src/putnam_1975_b5.lean index 6d152d35..0d0a580a 100644 --- a/lean4/src/putnam_1975_b5.lean +++ b/lean4/src/putnam_1975_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex Matrix Filter Topology Multiset diff --git a/lean4/src/putnam_1975_b6.lean b/lean4/src/putnam_1975_b6.lean index a9059fdc..64e6f0b4 100644 --- a/lean4/src/putnam_1975_b6.lean +++ b/lean4/src/putnam_1975_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Real Complex Matrix Filter Topology Multiset diff --git a/lean4/src/putnam_1976_a2.lean b/lean4/src/putnam_1976_a2.lean index 8d2d3f22..3e1e04a2 100644 --- a/lean4/src/putnam_1976_a2.lean +++ b/lean4/src/putnam_1976_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial diff --git a/lean4/src/putnam_1976_a3.lean b/lean4/src/putnam_1976_a3.lean index 25733455..87f40079 100644 --- a/lean4/src/putnam_1976_a3.lean +++ b/lean4/src/putnam_1976_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1976_a3_solution : Set (ℕ × ℕ × ℕ × ℕ) := sorry -- {(3, 2, 2, 3), (2, 3, 3, 2)} diff --git a/lean4/src/putnam_1976_a4.lean b/lean4/src/putnam_1976_a4.lean index af683b48..73c1eefa 100644 --- a/lean4/src/putnam_1976_a4.lean +++ b/lean4/src/putnam_1976_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_1976_a6.lean b/lean4/src/putnam_1976_a6.lean index 3f594618..3c0d1203 100644 --- a/lean4/src/putnam_1976_a6.lean +++ b/lean4/src/putnam_1976_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_1976_b1.lean b/lean4/src/putnam_1976_b1.lean index afe36f0e..fc4741bb 100644 --- a/lean4/src/putnam_1976_b1.lean +++ b/lean4/src/putnam_1976_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Filter Topology diff --git a/lean4/src/putnam_1976_b2.lean b/lean4/src/putnam_1976_b2.lean index e5bdc630..72aeeb9e 100644 --- a/lean4/src/putnam_1976_b2.lean +++ b/lean4/src/putnam_1976_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Filter Topology diff --git a/lean4/src/putnam_1976_b3.lean b/lean4/src/putnam_1976_b3.lean index dab28c18..c06d906c 100644 --- a/lean4/src/putnam_1976_b3.lean +++ b/lean4/src/putnam_1976_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Filter Topology ProbabilityTheory MeasureTheory diff --git a/lean4/src/putnam_1976_b5.lean b/lean4/src/putnam_1976_b5.lean index cb068f44..0b23bd68 100644 --- a/lean4/src/putnam_1976_b5.lean +++ b/lean4/src/putnam_1976_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Filter Topology ProbabilityTheory MeasureTheory diff --git a/lean4/src/putnam_1976_b6.lean b/lean4/src/putnam_1976_b6.lean index f5bc6817..75647031 100644 --- a/lean4/src/putnam_1976_b6.lean +++ b/lean4/src/putnam_1976_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial Filter Topology ProbabilityTheory MeasureTheory diff --git a/lean4/src/putnam_1977_a1.lean b/lean4/src/putnam_1977_a1.lean index 7142c9a1..6b6c30cc 100644 --- a/lean4/src/putnam_1977_a1.lean +++ b/lean4/src/putnam_1977_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_1977_a1_solution : ℝ := sorry -- -7 / 8 diff --git a/lean4/src/putnam_1977_a2.lean b/lean4/src/putnam_1977_a2.lean index cd865e14..8c013507 100644 --- a/lean4/src/putnam_1977_a2.lean +++ b/lean4/src/putnam_1977_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1977_a2_solution : ℝ → ℝ → ℝ → ℝ → Prop := sorry -- fun a b c d ↦ d = a ∧ b = -c ∨ d = b ∧ a = -c ∨ d = c ∧ a = -b diff --git a/lean4/src/putnam_1977_a3.lean b/lean4/src/putnam_1977_a3.lean index 074f58f4..c61fbb7d 100644 --- a/lean4/src/putnam_1977_a3.lean +++ b/lean4/src/putnam_1977_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1977_a3_solution : (ℝ → ℝ) → (ℝ → ℝ) → (ℝ → ℝ) := sorry -- fun f g x ↦ g x - f (x - 3) + f (x - 1) + f (x + 1) - f (x + 3) diff --git a/lean4/src/putnam_1977_a4.lean b/lean4/src/putnam_1977_a4.lean index ac14bc5e..349be510 100644 --- a/lean4/src/putnam_1977_a4.lean +++ b/lean4/src/putnam_1977_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open RingHom Set diff --git a/lean4/src/putnam_1977_a5.lean b/lean4/src/putnam_1977_a5.lean index 75ab81eb..baaa9413 100644 --- a/lean4/src/putnam_1977_a5.lean +++ b/lean4/src/putnam_1977_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open RingHom Set Nat diff --git a/lean4/src/putnam_1977_a6.lean b/lean4/src/putnam_1977_a6.lean index 6568b92e..d9b477ce 100644 --- a/lean4/src/putnam_1977_a6.lean +++ b/lean4/src/putnam_1977_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open RingHom Set Nat diff --git a/lean4/src/putnam_1977_b1.lean b/lean4/src/putnam_1977_b1.lean index cf8eba63..56e2ebc4 100644 --- a/lean4/src/putnam_1977_b1.lean +++ b/lean4/src/putnam_1977_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open RingHom Set Nat Filter Topology diff --git a/lean4/src/putnam_1977_b3.lean b/lean4/src/putnam_1977_b3.lean index 5b259383..c485075d 100644 --- a/lean4/src/putnam_1977_b3.lean +++ b/lean4/src/putnam_1977_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open RingHom Set Nat Filter Topology diff --git a/lean4/src/putnam_1977_b5.lean b/lean4/src/putnam_1977_b5.lean index 71b1018c..ebb1a37c 100644 --- a/lean4/src/putnam_1977_b5.lean +++ b/lean4/src/putnam_1977_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open RingHom Set Nat Filter Topology diff --git a/lean4/src/putnam_1977_b6.lean b/lean4/src/putnam_1977_b6.lean index 6b3da7c0..18d3241e 100644 --- a/lean4/src/putnam_1977_b6.lean +++ b/lean4/src/putnam_1977_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open RingHom Set Nat Filter Topology diff --git a/lean4/src/putnam_1978_a1.lean b/lean4/src/putnam_1978_a1.lean index 72371f34..0dfd7d41 100644 --- a/lean4/src/putnam_1978_a1.lean +++ b/lean4/src/putnam_1978_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $S = \{1, 4, 7, 10, 13, 16, \dots , 100\}$. Let $T$ be a subset of $20$ elements of $S$. Show that we can find two distinct elements of $T$ with sum $104$. diff --git a/lean4/src/putnam_1978_a2.lean b/lean4/src/putnam_1978_a2.lean index cdc74e54..94270812 100644 --- a/lean4/src/putnam_1978_a2.lean +++ b/lean4/src/putnam_1978_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $A$ be the real $n \times n$ matrix $(a_{ij})$ where $a_{ij} = a$ for $i < j$, $b \; (\neq a)$ for $i > j$, and $c_i$ for $i = j$. Show that $\det A = \frac{b p(a) - a p(b)}{b - a}$, where $p(x) = \prod_{i=1}^n (c_i - x)$. diff --git a/lean4/src/putnam_1978_a3.lean b/lean4/src/putnam_1978_a3.lean index c21d20e8..ec08e9fc 100644 --- a/lean4/src/putnam_1978_a3.lean +++ b/lean4/src/putnam_1978_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Polynomial diff --git a/lean4/src/putnam_1978_a4.lean b/lean4/src/putnam_1978_a4.lean index 93025f5c..769c030c 100644 --- a/lean4/src/putnam_1978_a4.lean +++ b/lean4/src/putnam_1978_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1978_a5.lean b/lean4/src/putnam_1978_a5.lean index 45ef5d00..fffeb3e7 100644 --- a/lean4/src/putnam_1978_a5.lean +++ b/lean4/src/putnam_1978_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Real diff --git a/lean4/src/putnam_1978_a6.lean b/lean4/src/putnam_1978_a6.lean index baae166c..6e0a8f9d 100644 --- a/lean4/src/putnam_1978_a6.lean +++ b/lean4/src/putnam_1978_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Real diff --git a/lean4/src/putnam_1978_b2.lean b/lean4/src/putnam_1978_b2.lean index b5b2581a..446e05b4 100644 --- a/lean4/src/putnam_1978_b2.lean +++ b/lean4/src/putnam_1978_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Real diff --git a/lean4/src/putnam_1978_b3.lean b/lean4/src/putnam_1978_b3.lean index 8ea7f2f2..e1915d82 100644 --- a/lean4/src/putnam_1978_b3.lean +++ b/lean4/src/putnam_1978_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Real Filter Topology Polynomial diff --git a/lean4/src/putnam_1978_b4.lean b/lean4/src/putnam_1978_b4.lean index 9f65d75b..08856fe2 100644 --- a/lean4/src/putnam_1978_b4.lean +++ b/lean4/src/putnam_1978_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Real Filter Topology Polynomial diff --git a/lean4/src/putnam_1978_b5.lean b/lean4/src/putnam_1978_b5.lean index 7a3dda3e..9e85d88a 100644 --- a/lean4/src/putnam_1978_b5.lean +++ b/lean4/src/putnam_1978_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Real Filter Topology Polynomial diff --git a/lean4/src/putnam_1978_b6.lean b/lean4/src/putnam_1978_b6.lean index 3f42f7a3..06ccc1f5 100644 --- a/lean4/src/putnam_1978_b6.lean +++ b/lean4/src/putnam_1978_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Real Filter Topology Polynomial diff --git a/lean4/src/putnam_1979_a1.lean b/lean4/src/putnam_1979_a1.lean index 80456f68..81905d07 100644 --- a/lean4/src/putnam_1979_a1.lean +++ b/lean4/src/putnam_1979_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1979_a1_solution : Multiset ℕ := sorry -- Multiset.replicate 659 3 + {2} diff --git a/lean4/src/putnam_1979_a2.lean b/lean4/src/putnam_1979_a2.lean index d7f7ef58..a3604f04 100644 --- a/lean4/src/putnam_1979_a2.lean +++ b/lean4/src/putnam_1979_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1979_a2_solution : ℝ → Prop := sorry -- fun k : ℝ => k ≥ 0 diff --git a/lean4/src/putnam_1979_a3.lean b/lean4/src/putnam_1979_a3.lean index 253def7f..144b48b3 100644 --- a/lean4/src/putnam_1979_a3.lean +++ b/lean4/src/putnam_1979_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1979_a3_solution : (ℝ × ℝ) → Prop := sorry -- fun (a, b) => ∃ m : ℤ, a = m ∧ b = m diff --git a/lean4/src/putnam_1979_a4.lean b/lean4/src/putnam_1979_a4.lean index 1ed96e36..f4d706d0 100644 --- a/lean4/src/putnam_1979_a4.lean +++ b/lean4/src/putnam_1979_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1979_a5.lean b/lean4/src/putnam_1979_a5.lean index e71b0470..68b3ae6e 100644 --- a/lean4/src/putnam_1979_a5.lean +++ b/lean4/src/putnam_1979_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1979_a6.lean b/lean4/src/putnam_1979_a6.lean index eedc6ff8..fb47d6d8 100644 --- a/lean4/src/putnam_1979_a6.lean +++ b/lean4/src/putnam_1979_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1979_b2.lean b/lean4/src/putnam_1979_b2.lean index 8107e25f..165490fa 100644 --- a/lean4/src/putnam_1979_b2.lean +++ b/lean4/src/putnam_1979_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Topology Filter diff --git a/lean4/src/putnam_1979_b3.lean b/lean4/src/putnam_1979_b3.lean index 7ba152dc..a7b08e78 100644 --- a/lean4/src/putnam_1979_b3.lean +++ b/lean4/src/putnam_1979_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Topology Filter Polynomial diff --git a/lean4/src/putnam_1979_b5.lean b/lean4/src/putnam_1979_b5.lean index 9d5ca403..61b0c54c 100644 --- a/lean4/src/putnam_1979_b5.lean +++ b/lean4/src/putnam_1979_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Topology Filter Polynomial MeasureTheory diff --git a/lean4/src/putnam_1979_b6.lean b/lean4/src/putnam_1979_b6.lean index 641c78d3..e92f04ff 100644 --- a/lean4/src/putnam_1979_b6.lean +++ b/lean4/src/putnam_1979_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Topology Filter Polynomial MeasureTheory diff --git a/lean4/src/putnam_1980_a2.lean b/lean4/src/putnam_1980_a2.lean index 6f1285a6..db785780 100644 --- a/lean4/src/putnam_1980_a2.lean +++ b/lean4/src/putnam_1980_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1980_a2_solution : ℕ → ℕ → ℕ := sorry -- (fun r s : ℕ => (1 + 4 * r + 6 * r ^ 2) * (1 + 4 * s + 6 * s ^ 2)) diff --git a/lean4/src/putnam_1980_a3.lean b/lean4/src/putnam_1980_a3.lean index 894b2b79..65e4373e 100644 --- a/lean4/src/putnam_1980_a3.lean +++ b/lean4/src/putnam_1980_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_1980_a3_solution : ℝ := sorry -- Real.pi / 4 diff --git a/lean4/src/putnam_1980_a4.lean b/lean4/src/putnam_1980_a4.lean index 920781c1..4bbb535a 100644 --- a/lean4/src/putnam_1980_a4.lean +++ b/lean4/src/putnam_1980_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- \begin{enumerate} diff --git a/lean4/src/putnam_1980_a5.lean b/lean4/src/putnam_1980_a5.lean index fd10279a..1faf07ca 100644 --- a/lean4/src/putnam_1980_a5.lean +++ b/lean4/src/putnam_1980_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $P(t)$ be a nonconstant polynomial with real coefficients. Prove that the system of simultaneous equations $0=\int_0^xP(t)\sin t\,dt=\int_0^xP(t)\cos t\,dt$ has only finitely many real solutions $x$. diff --git a/lean4/src/putnam_1980_a6.lean b/lean4/src/putnam_1980_a6.lean index 30fba095..65f2ac41 100644 --- a/lean4/src/putnam_1980_a6.lean +++ b/lean4/src/putnam_1980_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators -- Note: uses (ℝ → ℝ) instead of (Set.Icc (0 : ℝ) 1 → ℝ) noncomputable abbrev putnam_1980_a6_solution : ℝ := sorry diff --git a/lean4/src/putnam_1980_b1.lean b/lean4/src/putnam_1980_b1.lean index 66c16c3f..bf9a4785 100644 --- a/lean4/src/putnam_1980_b1.lean +++ b/lean4/src/putnam_1980_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real diff --git a/lean4/src/putnam_1980_b3.lean b/lean4/src/putnam_1980_b3.lean index aff41b02..c3f14670 100644 --- a/lean4/src/putnam_1980_b3.lean +++ b/lean4/src/putnam_1980_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1980_b3_solution : Set ℝ := sorry -- {a : ℝ | a ≥ 3} diff --git a/lean4/src/putnam_1980_b4.lean b/lean4/src/putnam_1980_b4.lean index 5931fa1a..80ddae64 100644 --- a/lean4/src/putnam_1980_b4.lean +++ b/lean4/src/putnam_1980_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $X$ be a finite set with at least $10$ elements; for each $i \in \{0, 1, ..., 1065\}$, let $A_i \subseteq X$ satisfy $|A_i| > \frac{1}{2}|X|$. Prove that there exist $10$ elements $x_1, x_2, \dots, x_{10} \in X$ such that each $A_i$ contains at least one of $x_1, x_2, \dots, x_{10}$. diff --git a/lean4/src/putnam_1980_b5.lean b/lean4/src/putnam_1980_b5.lean index 618d3d6d..c9d7ba03 100644 --- a/lean4/src/putnam_1980_b5.lean +++ b/lean4/src/putnam_1980_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1980_b6.lean b/lean4/src/putnam_1980_b6.lean index 17e04d38..493d8051 100644 --- a/lean4/src/putnam_1980_b6.lean +++ b/lean4/src/putnam_1980_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1981_a1.lean b/lean4/src/putnam_1981_a1.lean index 51a41ab8..911f9273 100644 --- a/lean4/src/putnam_1981_a1.lean +++ b/lean4/src/putnam_1981_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1981_a3.lean b/lean4/src/putnam_1981_a3.lean index 4bd03e02..80c2114a 100644 --- a/lean4/src/putnam_1981_a3.lean +++ b/lean4/src/putnam_1981_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1981_a5.lean b/lean4/src/putnam_1981_a5.lean index 3cbd6444..8ef436e1 100644 --- a/lean4/src/putnam_1981_a5.lean +++ b/lean4/src/putnam_1981_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1981_b1.lean b/lean4/src/putnam_1981_b1.lean index 94c2340a..077aabd8 100644 --- a/lean4/src/putnam_1981_b1.lean +++ b/lean4/src/putnam_1981_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1981_b2.lean b/lean4/src/putnam_1981_b2.lean index 5da3d8f3..c74c1236 100644 --- a/lean4/src/putnam_1981_b2.lean +++ b/lean4/src/putnam_1981_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1981_b3.lean b/lean4/src/putnam_1981_b3.lean index 6d68c0a8..e6aedd74 100644 --- a/lean4/src/putnam_1981_b3.lean +++ b/lean4/src/putnam_1981_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1981_b4.lean b/lean4/src/putnam_1981_b4.lean index a5402222..5cb5f78f 100644 --- a/lean4/src/putnam_1981_b4.lean +++ b/lean4/src/putnam_1981_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1981_b5.lean b/lean4/src/putnam_1981_b5.lean index 06c07a57..e796e955 100644 --- a/lean4/src/putnam_1981_b5.lean +++ b/lean4/src/putnam_1981_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Polynomial Function diff --git a/lean4/src/putnam_1982_a2.lean b/lean4/src/putnam_1982_a2.lean index e2be2867..9e216619 100644 --- a/lean4/src/putnam_1982_a2.lean +++ b/lean4/src/putnam_1982_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology Polynomial Real diff --git a/lean4/src/putnam_1982_a3.lean b/lean4/src/putnam_1982_a3.lean index 2f7ec8f3..c0627f99 100644 --- a/lean4/src/putnam_1982_a3.lean +++ b/lean4/src/putnam_1982_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology Polynomial Real diff --git a/lean4/src/putnam_1982_a4.lean b/lean4/src/putnam_1982_a4.lean index fc9b25db..613fef7a 100644 --- a/lean4/src/putnam_1982_a4.lean +++ b/lean4/src/putnam_1982_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Filter Topology diff --git a/lean4/src/putnam_1982_a5.lean b/lean4/src/putnam_1982_a5.lean index 9e1e919c..be613e8a 100644 --- a/lean4/src/putnam_1982_a5.lean +++ b/lean4/src/putnam_1982_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $a, b, c, d$ be positive integers satisfying $a + c \leq 1982$ and $\frac{a}{b} + \frac{c}{d} < 1$. Prove that $1 - \frac{a}{b} - \frac{c}{d} > \frac{1}{1983^3}$. diff --git a/lean4/src/putnam_1982_a6.lean b/lean4/src/putnam_1982_a6.lean index a024480c..d76da022 100644 --- a/lean4/src/putnam_1982_a6.lean +++ b/lean4/src/putnam_1982_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology Polynomial Real diff --git a/lean4/src/putnam_1982_b2.lean b/lean4/src/putnam_1982_b2.lean index b2978021..5bd67667 100644 --- a/lean4/src/putnam_1982_b2.lean +++ b/lean4/src/putnam_1982_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology Polynomial Real diff --git a/lean4/src/putnam_1982_b3.lean b/lean4/src/putnam_1982_b3.lean index 32d204df..c8417e91 100644 --- a/lean4/src/putnam_1982_b3.lean +++ b/lean4/src/putnam_1982_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology Polynomial Real diff --git a/lean4/src/putnam_1982_b4.lean b/lean4/src/putnam_1982_b4.lean index c32a4ce1..4fadfea0 100644 --- a/lean4/src/putnam_1982_b4.lean +++ b/lean4/src/putnam_1982_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology Polynomial Real diff --git a/lean4/src/putnam_1982_b5.lean b/lean4/src/putnam_1982_b5.lean index b72c2740..c0caaf0d 100644 --- a/lean4/src/putnam_1982_b5.lean +++ b/lean4/src/putnam_1982_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Filter Topology Polynomial Real diff --git a/lean4/src/putnam_1983_a1.lean b/lean4/src/putnam_1983_a1.lean index a7c44b4f..055d2a6e 100644 --- a/lean4/src/putnam_1983_a1.lean +++ b/lean4/src/putnam_1983_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1983_a1_solution : ℕ := sorry -- 2301 diff --git a/lean4/src/putnam_1983_a3.lean b/lean4/src/putnam_1983_a3.lean index b6570efc..a755bc1b 100644 --- a/lean4/src/putnam_1983_a3.lean +++ b/lean4/src/putnam_1983_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $p$ be in the set $\{3,5,7,11,\dots\}$ of odd primes and let $F(n)=1+2n+3n^2+\dots+(p-1)n^{p-2}$. Prove that if $a$ and $b$ are distinct integers in $\{0,1,2,\dots,p-1\}$ then $F(a)$ and $F(b)$ are not congruent modulo $p$, that is, $F(a)-F(b)$ is not exactly divisible by $p$. diff --git a/lean4/src/putnam_1983_a4.lean b/lean4/src/putnam_1983_a4.lean index a1d1a691..22c50827 100644 --- a/lean4/src/putnam_1983_a4.lean +++ b/lean4/src/putnam_1983_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_1983_a5.lean b/lean4/src/putnam_1983_a5.lean index 75218fa6..ab17938b 100644 --- a/lean4/src/putnam_1983_a5.lean +++ b/lean4/src/putnam_1983_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_1983_a6.lean b/lean4/src/putnam_1983_a6.lean index 61d814a2..d4580ee7 100644 --- a/lean4/src/putnam_1983_a6.lean +++ b/lean4/src/putnam_1983_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Filter Topology Real diff --git a/lean4/src/putnam_1983_b2.lean b/lean4/src/putnam_1983_b2.lean index 04076aab..e018606d 100644 --- a/lean4/src/putnam_1983_b2.lean +++ b/lean4/src/putnam_1983_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Filter Topology Real diff --git a/lean4/src/putnam_1983_b4.lean b/lean4/src/putnam_1983_b4.lean index cbd70e0f..f05e9ad4 100644 --- a/lean4/src/putnam_1983_b4.lean +++ b/lean4/src/putnam_1983_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Real diff --git a/lean4/src/putnam_1983_b5.lean b/lean4/src/putnam_1983_b5.lean index 3f06299d..8be90b71 100644 --- a/lean4/src/putnam_1983_b5.lean +++ b/lean4/src/putnam_1983_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Filter Topology Real diff --git a/lean4/src/putnam_1983_b6.lean b/lean4/src/putnam_1983_b6.lean index 08743fc1..822ffaa2 100644 --- a/lean4/src/putnam_1983_b6.lean +++ b/lean4/src/putnam_1983_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Filter Topology Real Polynomial diff --git a/lean4/src/putnam_1984_a2.lean b/lean4/src/putnam_1984_a2.lean index 45b3027e..29338b7c 100644 --- a/lean4/src/putnam_1984_a2.lean +++ b/lean4/src/putnam_1984_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1984_a2_solution : ℚ := sorry -- 2 diff --git a/lean4/src/putnam_1984_a3.lean b/lean4/src/putnam_1984_a3.lean index 78999ef3..493aab2c 100644 --- a/lean4/src/putnam_1984_a3.lean +++ b/lean4/src/putnam_1984_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_1984_a5.lean b/lean4/src/putnam_1984_a5.lean index 09bbcd64..3d358162 100644 --- a/lean4/src/putnam_1984_a5.lean +++ b/lean4/src/putnam_1984_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_1984_a6.lean b/lean4/src/putnam_1984_a6.lean index 9cd8e4d6..7670fb7a 100644 --- a/lean4/src/putnam_1984_a6.lean +++ b/lean4/src/putnam_1984_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Function Nat diff --git a/lean4/src/putnam_1984_b1.lean b/lean4/src/putnam_1984_b1.lean index d90a8de4..22502c53 100644 --- a/lean4/src/putnam_1984_b1.lean +++ b/lean4/src/putnam_1984_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_1984_b2.lean b/lean4/src/putnam_1984_b2.lean index 109f71ec..26529709 100644 --- a/lean4/src/putnam_1984_b2.lean +++ b/lean4/src/putnam_1984_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_1984_b3.lean b/lean4/src/putnam_1984_b3.lean index acaaf8af..149755a0 100644 --- a/lean4/src/putnam_1984_b3.lean +++ b/lean4/src/putnam_1984_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_1984_b5.lean b/lean4/src/putnam_1984_b5.lean index 113c0a59..244c189a 100644 --- a/lean4/src/putnam_1984_b5.lean +++ b/lean4/src/putnam_1984_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_1985_a1.lean b/lean4/src/putnam_1985_a1.lean index 22d2b37e..5bb6342b 100644 --- a/lean4/src/putnam_1985_a1.lean +++ b/lean4/src/putnam_1985_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1985_a3.lean b/lean4/src/putnam_1985_a3.lean index 0673f9cc..0729b0ea 100644 --- a/lean4/src/putnam_1985_a3.lean +++ b/lean4/src/putnam_1985_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real diff --git a/lean4/src/putnam_1985_a4.lean b/lean4/src/putnam_1985_a4.lean index c47e6f61..3aeccd4d 100644 --- a/lean4/src/putnam_1985_a4.lean +++ b/lean4/src/putnam_1985_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real diff --git a/lean4/src/putnam_1985_a5.lean b/lean4/src/putnam_1985_a5.lean index 4d68ef82..0375f1e6 100644 --- a/lean4/src/putnam_1985_a5.lean +++ b/lean4/src/putnam_1985_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real diff --git a/lean4/src/putnam_1985_a6.lean b/lean4/src/putnam_1985_a6.lean index 61a1dd52..c543fb29 100644 --- a/lean4/src/putnam_1985_a6.lean +++ b/lean4/src/putnam_1985_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real Polynomial diff --git a/lean4/src/putnam_1985_b1.lean b/lean4/src/putnam_1985_b1.lean index e23c5a3e..d4cb4172 100644 --- a/lean4/src/putnam_1985_b1.lean +++ b/lean4/src/putnam_1985_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real Polynomial Function diff --git a/lean4/src/putnam_1985_b2.lean b/lean4/src/putnam_1985_b2.lean index 2bef27df..c44ae17f 100644 --- a/lean4/src/putnam_1985_b2.lean +++ b/lean4/src/putnam_1985_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real Polynomial Function diff --git a/lean4/src/putnam_1985_b3.lean b/lean4/src/putnam_1985_b3.lean index 3e397b44..616cbb5f 100644 --- a/lean4/src/putnam_1985_b3.lean +++ b/lean4/src/putnam_1985_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real Polynomial Function diff --git a/lean4/src/putnam_1985_b5.lean b/lean4/src/putnam_1985_b5.lean index b4d1cdda..405ee17d 100644 --- a/lean4/src/putnam_1985_b5.lean +++ b/lean4/src/putnam_1985_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real Polynomial Function diff --git a/lean4/src/putnam_1985_b6.lean b/lean4/src/putnam_1985_b6.lean index 610f8305..b32184b7 100644 --- a/lean4/src/putnam_1985_b6.lean +++ b/lean4/src/putnam_1985_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology Real Polynomial Function diff --git a/lean4/src/putnam_1986_a1.lean b/lean4/src/putnam_1986_a1.lean index aa840531..30fd6792 100644 --- a/lean4/src/putnam_1986_a1.lean +++ b/lean4/src/putnam_1986_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1986_a1_solution : ℝ := sorry -- 18 diff --git a/lean4/src/putnam_1986_a2.lean b/lean4/src/putnam_1986_a2.lean index 59b0da75..b8e71199 100644 --- a/lean4/src/putnam_1986_a2.lean +++ b/lean4/src/putnam_1986_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1986_a2_solution : ℕ := sorry -- 3 diff --git a/lean4/src/putnam_1986_a3.lean b/lean4/src/putnam_1986_a3.lean index d73b2c6c..281c6511 100644 --- a/lean4/src/putnam_1986_a3.lean +++ b/lean4/src/putnam_1986_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real diff --git a/lean4/src/putnam_1986_a4.lean b/lean4/src/putnam_1986_a4.lean index 7616e34e..d6869596 100644 --- a/lean4/src/putnam_1986_a4.lean +++ b/lean4/src/putnam_1986_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv diff --git a/lean4/src/putnam_1986_a5.lean b/lean4/src/putnam_1986_a5.lean index bce3d2e2..699b7ba6 100644 --- a/lean4/src/putnam_1986_a5.lean +++ b/lean4/src/putnam_1986_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv diff --git a/lean4/src/putnam_1986_a6.lean b/lean4/src/putnam_1986_a6.lean index f37343ec..b20e1f94 100644 --- a/lean4/src/putnam_1986_a6.lean +++ b/lean4/src/putnam_1986_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv diff --git a/lean4/src/putnam_1986_b1.lean b/lean4/src/putnam_1986_b1.lean index e0424e17..91ac83d9 100644 --- a/lean4/src/putnam_1986_b1.lean +++ b/lean4/src/putnam_1986_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv diff --git a/lean4/src/putnam_1986_b2.lean b/lean4/src/putnam_1986_b2.lean index 390bb1d4..e0c92ac4 100644 --- a/lean4/src/putnam_1986_b2.lean +++ b/lean4/src/putnam_1986_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv diff --git a/lean4/src/putnam_1986_b3.lean b/lean4/src/putnam_1986_b3.lean index d720fd3e..d7cc6765 100644 --- a/lean4/src/putnam_1986_b3.lean +++ b/lean4/src/putnam_1986_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv Polynomial diff --git a/lean4/src/putnam_1986_b4.lean b/lean4/src/putnam_1986_b4.lean index 347b5d0c..49a86eb3 100644 --- a/lean4/src/putnam_1986_b4.lean +++ b/lean4/src/putnam_1986_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv Polynomial Filter Topology diff --git a/lean4/src/putnam_1986_b5.lean b/lean4/src/putnam_1986_b5.lean index 35f21205..9c392bf1 100644 --- a/lean4/src/putnam_1986_b5.lean +++ b/lean4/src/putnam_1986_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv Polynomial Filter Topology MvPolynomial diff --git a/lean4/src/putnam_1986_b6.lean b/lean4/src/putnam_1986_b6.lean index 9a2cdc12..71d8b158 100644 --- a/lean4/src/putnam_1986_b6.lean +++ b/lean4/src/putnam_1986_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Real Equiv Polynomial Filter Topology MvPolynomial Matrix diff --git a/lean4/src/putnam_1987_a1.lean b/lean4/src/putnam_1987_a1.lean index 1aeadd14..c1693c04 100644 --- a/lean4/src/putnam_1987_a1.lean +++ b/lean4/src/putnam_1987_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Curves $A$, $B$, $C$, and $D$ are defined in the plane as follows: diff --git a/lean4/src/putnam_1987_a2.lean b/lean4/src/putnam_1987_a2.lean index 7b5924d9..6ced9af7 100644 --- a/lean4/src/putnam_1987_a2.lean +++ b/lean4/src/putnam_1987_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1987_a2_solution : ℕ := sorry -- 1984 diff --git a/lean4/src/putnam_1987_a4.lean b/lean4/src/putnam_1987_a4.lean index 5cd88143..cf0e16b8 100644 --- a/lean4/src/putnam_1987_a4.lean +++ b/lean4/src/putnam_1987_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real diff --git a/lean4/src/putnam_1987_a5.lean b/lean4/src/putnam_1987_a5.lean index 5fad17e1..aae45c50 100644 --- a/lean4/src/putnam_1987_a5.lean +++ b/lean4/src/putnam_1987_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real diff --git a/lean4/src/putnam_1987_a6.lean b/lean4/src/putnam_1987_a6.lean index da2ddc88..5978b608 100644 --- a/lean4/src/putnam_1987_a6.lean +++ b/lean4/src/putnam_1987_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real Nat diff --git a/lean4/src/putnam_1987_b1.lean b/lean4/src/putnam_1987_b1.lean index c972732b..a6052957 100644 --- a/lean4/src/putnam_1987_b1.lean +++ b/lean4/src/putnam_1987_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real Nat diff --git a/lean4/src/putnam_1987_b2.lean b/lean4/src/putnam_1987_b2.lean index 3293659e..74729cd6 100644 --- a/lean4/src/putnam_1987_b2.lean +++ b/lean4/src/putnam_1987_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real Nat diff --git a/lean4/src/putnam_1987_b3.lean b/lean4/src/putnam_1987_b3.lean index b2fff123..29dc8dc4 100644 --- a/lean4/src/putnam_1987_b3.lean +++ b/lean4/src/putnam_1987_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real Nat diff --git a/lean4/src/putnam_1987_b4.lean b/lean4/src/putnam_1987_b4.lean index 00f5c08d..e04325ce 100644 --- a/lean4/src/putnam_1987_b4.lean +++ b/lean4/src/putnam_1987_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real Nat Filter Topology diff --git a/lean4/src/putnam_1987_b5.lean b/lean4/src/putnam_1987_b5.lean index b2d70ea5..4c0f839a 100644 --- a/lean4/src/putnam_1987_b5.lean +++ b/lean4/src/putnam_1987_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real Nat Filter Topology diff --git a/lean4/src/putnam_1987_b6.lean b/lean4/src/putnam_1987_b6.lean index 284a006e..188bf387 100644 --- a/lean4/src/putnam_1987_b6.lean +++ b/lean4/src/putnam_1987_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Real Nat Filter Topology diff --git a/lean4/src/putnam_1988_a1.lean b/lean4/src/putnam_1988_a1.lean index 70bae3fc..e2c14f18 100644 --- a/lean4/src/putnam_1988_a1.lean +++ b/lean4/src/putnam_1988_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1988_a1_solution : ℝ := sorry -- 6 diff --git a/lean4/src/putnam_1988_a2.lean b/lean4/src/putnam_1988_a2.lean index ac1900b8..84e97a9e 100644 --- a/lean4/src/putnam_1988_a2.lean +++ b/lean4/src/putnam_1988_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_1988_a3.lean b/lean4/src/putnam_1988_a3.lean index a8726e55..2cb1b4ee 100644 --- a/lean4/src/putnam_1988_a3.lean +++ b/lean4/src/putnam_1988_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_a4.lean b/lean4/src/putnam_1988_a4.lean index 213d8f04..f9284d11 100644 --- a/lean4/src/putnam_1988_a4.lean +++ b/lean4/src/putnam_1988_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_a5.lean b/lean4/src/putnam_1988_a5.lean index 7d584e68..5f3cad51 100644 --- a/lean4/src/putnam_1988_a5.lean +++ b/lean4/src/putnam_1988_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_a6.lean b/lean4/src/putnam_1988_a6.lean index c5b36369..0931ab0f 100644 --- a/lean4/src/putnam_1988_a6.lean +++ b/lean4/src/putnam_1988_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_b1.lean b/lean4/src/putnam_1988_b1.lean index 1710edfa..42401a7c 100644 --- a/lean4/src/putnam_1988_b1.lean +++ b/lean4/src/putnam_1988_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_b2.lean b/lean4/src/putnam_1988_b2.lean index 22683c57..64a1fb93 100644 --- a/lean4/src/putnam_1988_b2.lean +++ b/lean4/src/putnam_1988_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_b3.lean b/lean4/src/putnam_1988_b3.lean index b5892363..06ff3610 100644 --- a/lean4/src/putnam_1988_b3.lean +++ b/lean4/src/putnam_1988_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_b4.lean b/lean4/src/putnam_1988_b4.lean index ca4c58ea..bf27f2a7 100644 --- a/lean4/src/putnam_1988_b4.lean +++ b/lean4/src/putnam_1988_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_b5.lean b/lean4/src/putnam_1988_b5.lean index a0a3dc86..5ac03603 100644 --- a/lean4/src/putnam_1988_b5.lean +++ b/lean4/src/putnam_1988_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1988_b6.lean b/lean4/src/putnam_1988_b6.lean index a8760098..80852362 100644 --- a/lean4/src/putnam_1988_b6.lean +++ b/lean4/src/putnam_1988_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Filter Topology diff --git a/lean4/src/putnam_1989_a1.lean b/lean4/src/putnam_1989_a1.lean index 52dd78d6..4b222162 100644 --- a/lean4/src/putnam_1989_a1.lean +++ b/lean4/src/putnam_1989_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1989_a1_solution : ℕ∞ := sorry -- 1 diff --git a/lean4/src/putnam_1989_a2.lean b/lean4/src/putnam_1989_a2.lean index 6ee337a7..1a985f08 100644 --- a/lean4/src/putnam_1989_a2.lean +++ b/lean4/src/putnam_1989_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_1989_a2_solution : ℝ → ℝ → ℝ := sorry -- (fun a b : ℝ => (Real.exp (a ^ 2 * b ^ 2) - 1) / (a * b)) diff --git a/lean4/src/putnam_1989_a3.lean b/lean4/src/putnam_1989_a3.lean index 1179157e..bac10ff9 100644 --- a/lean4/src/putnam_1989_a3.lean +++ b/lean4/src/putnam_1989_a3.lean @@ -1,5 +1,5 @@ import Mathlib -open BigOperators Complex +open Complex /-- Prove that if diff --git a/lean4/src/putnam_1989_a6.lean b/lean4/src/putnam_1989_a6.lean index 6f00a82a..b4348d8e 100644 --- a/lean4/src/putnam_1989_a6.lean +++ b/lean4/src/putnam_1989_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_1989_b1.lean b/lean4/src/putnam_1989_b1.lean index 293a1b7e..3fc5bc39 100644 --- a/lean4/src/putnam_1989_b1.lean +++ b/lean4/src/putnam_1989_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_1989_b2.lean b/lean4/src/putnam_1989_b2.lean index 34c75521..eb5bbee3 100644 --- a/lean4/src/putnam_1989_b2.lean +++ b/lean4/src/putnam_1989_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_1989_b3.lean b/lean4/src/putnam_1989_b3.lean index 748efad2..8bb9d026 100644 --- a/lean4/src/putnam_1989_b3.lean +++ b/lean4/src/putnam_1989_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Filter Topology diff --git a/lean4/src/putnam_1989_b4.lean b/lean4/src/putnam_1989_b4.lean index 8b16bec0..fc3673ec 100644 --- a/lean4/src/putnam_1989_b4.lean +++ b/lean4/src/putnam_1989_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Filter Topology Set diff --git a/lean4/src/putnam_1989_b6.lean b/lean4/src/putnam_1989_b6.lean index 85d4db46..e91a9056 100644 --- a/lean4/src/putnam_1989_b6.lean +++ b/lean4/src/putnam_1989_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Filter Topology Set diff --git a/lean4/src/putnam_1990_a1.lean b/lean4/src/putnam_1990_a1.lean index 128124a9..336fc49a 100644 --- a/lean4/src/putnam_1990_a1.lean +++ b/lean4/src/putnam_1990_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_a2.lean b/lean4/src/putnam_1990_a2.lean index 07ab2428..7a79cc1d 100644 --- a/lean4/src/putnam_1990_a2.lean +++ b/lean4/src/putnam_1990_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_a4.lean b/lean4/src/putnam_1990_a4.lean index a0ea526c..66419f0f 100644 --- a/lean4/src/putnam_1990_a4.lean +++ b/lean4/src/putnam_1990_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_a5.lean b/lean4/src/putnam_1990_a5.lean index 870d469f..55713e95 100644 --- a/lean4/src/putnam_1990_a5.lean +++ b/lean4/src/putnam_1990_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_a6.lean b/lean4/src/putnam_1990_a6.lean index ff520934..520d10c8 100644 --- a/lean4/src/putnam_1990_a6.lean +++ b/lean4/src/putnam_1990_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_b1.lean b/lean4/src/putnam_1990_b1.lean index c936b2df..83357c58 100644 --- a/lean4/src/putnam_1990_b1.lean +++ b/lean4/src/putnam_1990_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_b2.lean b/lean4/src/putnam_1990_b2.lean index 212d45b0..5d8162df 100644 --- a/lean4/src/putnam_1990_b2.lean +++ b/lean4/src/putnam_1990_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_b3.lean b/lean4/src/putnam_1990_b3.lean index 010ebe7e..5a57eaaa 100644 --- a/lean4/src/putnam_1990_b3.lean +++ b/lean4/src/putnam_1990_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_b4.lean b/lean4/src/putnam_1990_b4.lean index 65e0b0d0..47862816 100644 --- a/lean4/src/putnam_1990_b4.lean +++ b/lean4/src/putnam_1990_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Nat diff --git a/lean4/src/putnam_1990_b5.lean b/lean4/src/putnam_1990_b5.lean index 40afc454..3d78532b 100644 --- a/lean4/src/putnam_1990_b5.lean +++ b/lean4/src/putnam_1990_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Polynomial Topology Nat diff --git a/lean4/src/putnam_1991_a2.lean b/lean4/src/putnam_1991_a2.lean index b3df6ec7..6b941f02 100644 --- a/lean4/src/putnam_1991_a2.lean +++ b/lean4/src/putnam_1991_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_a3.lean b/lean4/src/putnam_1991_a3.lean index 7026e977..50590b6b 100644 --- a/lean4/src/putnam_1991_a3.lean +++ b/lean4/src/putnam_1991_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_a4.lean b/lean4/src/putnam_1991_a4.lean index fbd479bc..5e44ac87 100644 --- a/lean4/src/putnam_1991_a4.lean +++ b/lean4/src/putnam_1991_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter FiniteDimensional Metric Topology diff --git a/lean4/src/putnam_1991_a5.lean b/lean4/src/putnam_1991_a5.lean index 6375b4e5..704e40b5 100644 --- a/lean4/src/putnam_1991_a5.lean +++ b/lean4/src/putnam_1991_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_a6.lean b/lean4/src/putnam_1991_a6.lean index 109d62cb..8f7099e2 100644 --- a/lean4/src/putnam_1991_a6.lean +++ b/lean4/src/putnam_1991_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_b1.lean b/lean4/src/putnam_1991_b1.lean index b08e9e79..2dd2ddeb 100644 --- a/lean4/src/putnam_1991_b1.lean +++ b/lean4/src/putnam_1991_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_b2.lean b/lean4/src/putnam_1991_b2.lean index 6a0edd44..9243453c 100644 --- a/lean4/src/putnam_1991_b2.lean +++ b/lean4/src/putnam_1991_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_b4.lean b/lean4/src/putnam_1991_b4.lean index f7211238..93159870 100644 --- a/lean4/src/putnam_1991_b4.lean +++ b/lean4/src/putnam_1991_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_b5.lean b/lean4/src/putnam_1991_b5.lean index 1c91c689..9eacbef9 100644 --- a/lean4/src/putnam_1991_b5.lean +++ b/lean4/src/putnam_1991_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1991_b6.lean b/lean4/src/putnam_1991_b6.lean index 81168ca5..1754fa9f 100644 --- a/lean4/src/putnam_1991_b6.lean +++ b/lean4/src/putnam_1991_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1992_a1.lean b/lean4/src/putnam_1992_a1.lean index dee4bbce..2b72fa84 100644 --- a/lean4/src/putnam_1992_a1.lean +++ b/lean4/src/putnam_1992_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_1992_a2.lean b/lean4/src/putnam_1992_a2.lean index a9dc25b7..8a4874f0 100644 --- a/lean4/src/putnam_1992_a2.lean +++ b/lean4/src/putnam_1992_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_1992_a3.lean b/lean4/src/putnam_1992_a3.lean index f005cd86..c862e65e 100644 --- a/lean4/src/putnam_1992_a3.lean +++ b/lean4/src/putnam_1992_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_1992_a4.lean b/lean4/src/putnam_1992_a4.lean index 24d2bb18..e4201409 100644 --- a/lean4/src/putnam_1992_a4.lean +++ b/lean4/src/putnam_1992_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function diff --git a/lean4/src/putnam_1992_a5.lean b/lean4/src/putnam_1992_a5.lean index f87bb57d..fc0a2db0 100644 --- a/lean4/src/putnam_1992_a5.lean +++ b/lean4/src/putnam_1992_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function diff --git a/lean4/src/putnam_1992_b1.lean b/lean4/src/putnam_1992_b1.lean index 3d586807..415c456d 100644 --- a/lean4/src/putnam_1992_b1.lean +++ b/lean4/src/putnam_1992_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function diff --git a/lean4/src/putnam_1992_b2.lean b/lean4/src/putnam_1992_b2.lean index 00de2315..9506b67c 100644 --- a/lean4/src/putnam_1992_b2.lean +++ b/lean4/src/putnam_1992_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function Polynomial diff --git a/lean4/src/putnam_1992_b3.lean b/lean4/src/putnam_1992_b3.lean index ccb093e7..d3005a4a 100644 --- a/lean4/src/putnam_1992_b3.lean +++ b/lean4/src/putnam_1992_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function Polynomial diff --git a/lean4/src/putnam_1992_b4.lean b/lean4/src/putnam_1992_b4.lean index f1f0b387..b42caf9f 100644 --- a/lean4/src/putnam_1992_b4.lean +++ b/lean4/src/putnam_1992_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function Polynomial diff --git a/lean4/src/putnam_1992_b5.lean b/lean4/src/putnam_1992_b5.lean index 5b917989..84a37237 100644 --- a/lean4/src/putnam_1992_b5.lean +++ b/lean4/src/putnam_1992_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function Polynomial diff --git a/lean4/src/putnam_1992_b6.lean b/lean4/src/putnam_1992_b6.lean index 2752a674..4d181708 100644 --- a/lean4/src/putnam_1992_b6.lean +++ b/lean4/src/putnam_1992_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Function Polynomial diff --git a/lean4/src/putnam_1993_a1.lean b/lean4/src/putnam_1993_a1.lean index 84705a57..ea69c5f0 100644 --- a/lean4/src/putnam_1993_a1.lean +++ b/lean4/src/putnam_1993_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_1993_a1_solution : ℝ := sorry -- 4 / 9 diff --git a/lean4/src/putnam_1993_a2.lean b/lean4/src/putnam_1993_a2.lean index ed76be07..fbd93edc 100644 --- a/lean4/src/putnam_1993_a2.lean +++ b/lean4/src/putnam_1993_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $(x_n)_{n \geq 0}$ be a sequence of nonzero real numbers such that $x_n^2-x_{n-1}x_{n+1}=1$ for $n=1,2,3,\dots$. Prove there exists a real number $a$ such that $x_{n+1}=ax_n-x_{n-1}$ for all $n \geq 1$. diff --git a/lean4/src/putnam_1993_a3.lean b/lean4/src/putnam_1993_a3.lean index 2e77f2bc..aa762160 100644 --- a/lean4/src/putnam_1993_a3.lean +++ b/lean4/src/putnam_1993_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $\mathcal{P}_n$ be the set of subsets of $\{1,2,\dots,n\}$. Let $c(n,m)$ be the number of functions $f:\mathcal{P}_n \to \{1,2,\dots,m\}$ such that $f(A \cap B)=\min\{f(A),f(B)\}$. Prove that $c(n,m)=\sum_{j=1}^m j^n$. diff --git a/lean4/src/putnam_1993_a4.lean b/lean4/src/putnam_1993_a4.lean index d286faa7..ed0fd3e0 100644 --- a/lean4/src/putnam_1993_a4.lean +++ b/lean4/src/putnam_1993_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $x_1,x_2,\dots,x_{19}$ be positive integers each of which is less than or equal to $93$. Let $y_1,y_2,\dots,y_{93}$ be positive integers each of which is less than or equal to $19$. Prove that there exists a (nonempty) sum of some $x_i$'s equal to a sum of some $y_j$'s. diff --git a/lean4/src/putnam_1993_a5.lean b/lean4/src/putnam_1993_a5.lean index 15b15d7f..d0c9a381 100644 --- a/lean4/src/putnam_1993_a5.lean +++ b/lean4/src/putnam_1993_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Show that $\int_{-100}^{-10} (\frac{x^2-x}{x^3-3x+1})^2\,dx+\int_{\frac{1}{101}}^{\frac{1}{11}} (\frac{x^2-x}{x^3-3x+1})^2\,dx+\int_{\frac{101}{100}}^{\frac{11}{10}} (\frac{x^2-x}{x^3-3x+1})^2\,dx$ is a rational number. diff --git a/lean4/src/putnam_1993_a6.lean b/lean4/src/putnam_1993_a6.lean index f6a36277..3e0886d8 100644 --- a/lean4/src/putnam_1993_a6.lean +++ b/lean4/src/putnam_1993_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- The infinite sequence of $2$'s and $3$'s $2,3,3,2,3,3,3,2,3,3,3,2,3,3,2,3,3,3,2,3,3,3,2,3,3,3,2,3,3,2,3,3,3,2,\dots$ has the property that, if one forms a second sequence that records the number of $3$'s between successive $2$'s, the result is identical to the given sequence. Show that there exists a real number $r$ such that, for any $n$, the $n$th term of the sequence is $2$ if and only if $n=1+\lfloor rm \rfloor$ for some nonnegative integer $m$. (Note: $\lfloor x \rfloor$ denotes the largest integer less than or equal to $x$.) diff --git a/lean4/src/putnam_1993_b1.lean b/lean4/src/putnam_1993_b1.lean index 81c50b16..8880750c 100644 --- a/lean4/src/putnam_1993_b1.lean +++ b/lean4/src/putnam_1993_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1993_b1_solution : ℕ := sorry -- 3987 diff --git a/lean4/src/putnam_1993_b3.lean b/lean4/src/putnam_1993_b3.lean index 95fed668..fba4668f 100644 --- a/lean4/src/putnam_1993_b3.lean +++ b/lean4/src/putnam_1993_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1993_b3_solution : ℚ × ℚ := sorry -- (5 / 4, -1 / 4) diff --git a/lean4/src/putnam_1993_b4.lean b/lean4/src/putnam_1993_b4.lean index 7cdb39f0..20d28090 100644 --- a/lean4/src/putnam_1993_b4.lean +++ b/lean4/src/putnam_1993_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- The function $K(x,y)$ is positive and continuous for $0 \leq x \leq 1,0 \leq y \leq 1$, and the functions $f(x)$ and $g(x)$ are positive and continuous for $0 \leq x \leq 1$. Suppose that for all $x$, $0 \leq x \leq 1$, $\int_0^1 f(y)K(x,y)\,dy=g(x)$ and $\int_0^1 g(y)K(x,y)\,dy=f(x)$. Show that $f(x)=g(x)$ for $0 \leq x \leq 1$. diff --git a/lean4/src/putnam_1993_b5.lean b/lean4/src/putnam_1993_b5.lean index bbc4a71b..72ce9d63 100644 --- a/lean4/src/putnam_1993_b5.lean +++ b/lean4/src/putnam_1993_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Show there do not exist four points in the Euclidean plane such that the pairwise distances between the points are all odd integers. diff --git a/lean4/src/putnam_1993_b6.lean b/lean4/src/putnam_1993_b6.lean index b46c7a59..b8bb6d5f 100644 --- a/lean4/src/putnam_1993_b6.lean +++ b/lean4/src/putnam_1993_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators -- Note: uses (ℕ → (Fin 3 → ℕ)) instead of (Fin (N + 1) → (Fin 3 → ℕ)) /-- diff --git a/lean4/src/putnam_1994_a1.lean b/lean4/src/putnam_1994_a1.lean index 99884791..890908f4 100644 --- a/lean4/src/putnam_1994_a1.lean +++ b/lean4/src/putnam_1994_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_a3.lean b/lean4/src/putnam_1994_a3.lean index b9831608..0b73520e 100644 --- a/lean4/src/putnam_1994_a3.lean +++ b/lean4/src/putnam_1994_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_a4.lean b/lean4/src/putnam_1994_a4.lean index db8c37d0..aa58a316 100644 --- a/lean4/src/putnam_1994_a4.lean +++ b/lean4/src/putnam_1994_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_a5.lean b/lean4/src/putnam_1994_a5.lean index f27164f3..5d6bfde3 100644 --- a/lean4/src/putnam_1994_a5.lean +++ b/lean4/src/putnam_1994_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_a6.lean b/lean4/src/putnam_1994_a6.lean index f1982454..ac50cb17 100644 --- a/lean4/src/putnam_1994_a6.lean +++ b/lean4/src/putnam_1994_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Classical Filter Topology diff --git a/lean4/src/putnam_1994_b1.lean b/lean4/src/putnam_1994_b1.lean index 550c9ffa..48e64fde 100644 --- a/lean4/src/putnam_1994_b1.lean +++ b/lean4/src/putnam_1994_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_b2.lean b/lean4/src/putnam_1994_b2.lean index 75201369..9aad8c07 100644 --- a/lean4/src/putnam_1994_b2.lean +++ b/lean4/src/putnam_1994_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_b3.lean b/lean4/src/putnam_1994_b3.lean index ec69120f..16bfef66 100644 --- a/lean4/src/putnam_1994_b3.lean +++ b/lean4/src/putnam_1994_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_b4.lean b/lean4/src/putnam_1994_b4.lean index 86448a61..5f1f57c3 100644 --- a/lean4/src/putnam_1994_b4.lean +++ b/lean4/src/putnam_1994_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_b5.lean b/lean4/src/putnam_1994_b5.lean index 5b98038d..626b156d 100644 --- a/lean4/src/putnam_1994_b5.lean +++ b/lean4/src/putnam_1994_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1994_b6.lean b/lean4/src/putnam_1994_b6.lean index ee28f4c3..60663438 100644 --- a/lean4/src/putnam_1994_b6.lean +++ b/lean4/src/putnam_1994_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1995_a1.lean b/lean4/src/putnam_1995_a1.lean index f3ae5114..58a6f770 100644 --- a/lean4/src/putnam_1995_a1.lean +++ b/lean4/src/putnam_1995_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $S$ be a set of real numbers which is closed under multiplication (that is, if $a$ and $b$ are in $S$, then so is $ab$). Let $T$ and $U$ be disjoint subsets of $S$ whose union is $S$. Given that the product of any {\em three} (not necessarily distinct) elements of $T$ is in $T$ and that the product of any three elements of $U$ is in $U$, show that at least one of the two subsets $T,U$ is closed under multiplication. diff --git a/lean4/src/putnam_1995_a2.lean b/lean4/src/putnam_1995_a2.lean index 974af32a..66811580 100644 --- a/lean4/src/putnam_1995_a2.lean +++ b/lean4/src/putnam_1995_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real diff --git a/lean4/src/putnam_1995_a3.lean b/lean4/src/putnam_1995_a3.lean index dae507d2..1529270a 100644 --- a/lean4/src/putnam_1995_a3.lean +++ b/lean4/src/putnam_1995_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real diff --git a/lean4/src/putnam_1995_a4.lean b/lean4/src/putnam_1995_a4.lean index 73f28113..f5794c8a 100644 --- a/lean4/src/putnam_1995_a4.lean +++ b/lean4/src/putnam_1995_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real diff --git a/lean4/src/putnam_1995_a5.lean b/lean4/src/putnam_1995_a5.lean index 05461ff2..c9953696 100644 --- a/lean4/src/putnam_1995_a5.lean +++ b/lean4/src/putnam_1995_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real diff --git a/lean4/src/putnam_1995_a6.lean b/lean4/src/putnam_1995_a6.lean index 73f181bb..96175b80 100644 --- a/lean4/src/putnam_1995_a6.lean +++ b/lean4/src/putnam_1995_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real diff --git a/lean4/src/putnam_1995_b1.lean b/lean4/src/putnam_1995_b1.lean index 1cdde8c7..f377d2ea 100644 --- a/lean4/src/putnam_1995_b1.lean +++ b/lean4/src/putnam_1995_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real Nat diff --git a/lean4/src/putnam_1995_b3.lean b/lean4/src/putnam_1995_b3.lean index f4936ab5..9d8e5d23 100644 --- a/lean4/src/putnam_1995_b3.lean +++ b/lean4/src/putnam_1995_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real Nat diff --git a/lean4/src/putnam_1995_b4.lean b/lean4/src/putnam_1995_b4.lean index e2405d83..4c3eb646 100644 --- a/lean4/src/putnam_1995_b4.lean +++ b/lean4/src/putnam_1995_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real Nat diff --git a/lean4/src/putnam_1995_b6.lean b/lean4/src/putnam_1995_b6.lean index 2e6846f7..7e533c96 100644 --- a/lean4/src/putnam_1995_b6.lean +++ b/lean4/src/putnam_1995_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Real Nat diff --git a/lean4/src/putnam_1996_a2.lean b/lean4/src/putnam_1996_a2.lean index d5ec02fc..550de80b 100644 --- a/lean4/src/putnam_1996_a2.lean +++ b/lean4/src/putnam_1996_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Metric diff --git a/lean4/src/putnam_1996_a3.lean b/lean4/src/putnam_1996_a3.lean index b129349d..c0f26df3 100644 --- a/lean4/src/putnam_1996_a3.lean +++ b/lean4/src/putnam_1996_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_1996_a3_solution : Prop := sorry -- False diff --git a/lean4/src/putnam_1996_a4.lean b/lean4/src/putnam_1996_a4.lean index c3771b9e..c3c1cee5 100644 --- a/lean4/src/putnam_1996_a4.lean +++ b/lean4/src/putnam_1996_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function diff --git a/lean4/src/putnam_1996_a5.lean b/lean4/src/putnam_1996_a5.lean index 78ed5a58..36913d34 100644 --- a/lean4/src/putnam_1996_a5.lean +++ b/lean4/src/putnam_1996_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function diff --git a/lean4/src/putnam_1996_a6.lean b/lean4/src/putnam_1996_a6.lean index 772254c0..8346210a 100644 --- a/lean4/src/putnam_1996_a6.lean +++ b/lean4/src/putnam_1996_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function diff --git a/lean4/src/putnam_1996_b1.lean b/lean4/src/putnam_1996_b1.lean index 4625512f..6b03b653 100644 --- a/lean4/src/putnam_1996_b1.lean +++ b/lean4/src/putnam_1996_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function diff --git a/lean4/src/putnam_1996_b2.lean b/lean4/src/putnam_1996_b2.lean index 68852858..d81441ef 100644 --- a/lean4/src/putnam_1996_b2.lean +++ b/lean4/src/putnam_1996_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function diff --git a/lean4/src/putnam_1996_b3.lean b/lean4/src/putnam_1996_b3.lean index 0116b7cb..fc067699 100644 --- a/lean4/src/putnam_1996_b3.lean +++ b/lean4/src/putnam_1996_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function diff --git a/lean4/src/putnam_1996_b4.lean b/lean4/src/putnam_1996_b4.lean index 36d85f58..e97ceedb 100644 --- a/lean4/src/putnam_1996_b4.lean +++ b/lean4/src/putnam_1996_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Nat diff --git a/lean4/src/putnam_1996_b5.lean b/lean4/src/putnam_1996_b5.lean index 25216b6e..41a61aef 100644 --- a/lean4/src/putnam_1996_b5.lean +++ b/lean4/src/putnam_1996_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Nat diff --git a/lean4/src/putnam_1997_a3.lean b/lean4/src/putnam_1997_a3.lean index f2901160..d27e743e 100644 --- a/lean4/src/putnam_1997_a3.lean +++ b/lean4/src/putnam_1997_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1997_a4.lean b/lean4/src/putnam_1997_a4.lean index 9cd30859..e2950bf5 100644 --- a/lean4/src/putnam_1997_a4.lean +++ b/lean4/src/putnam_1997_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1997_a5.lean b/lean4/src/putnam_1997_a5.lean index 2c4a0749..5862a948 100644 --- a/lean4/src/putnam_1997_a5.lean +++ b/lean4/src/putnam_1997_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1997_a6.lean b/lean4/src/putnam_1997_a6.lean index 40bf7873..03dda8c0 100644 --- a/lean4/src/putnam_1997_a6.lean +++ b/lean4/src/putnam_1997_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1997_b1.lean b/lean4/src/putnam_1997_b1.lean index ad6e582f..07483850 100644 --- a/lean4/src/putnam_1997_b1.lean +++ b/lean4/src/putnam_1997_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_1997_b2.lean b/lean4/src/putnam_1997_b2.lean index 9645959a..76eadbf7 100644 --- a/lean4/src/putnam_1997_b2.lean +++ b/lean4/src/putnam_1997_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Bornology Set diff --git a/lean4/src/putnam_1997_b3.lean b/lean4/src/putnam_1997_b3.lean index f4e47fd9..01eef1d2 100644 --- a/lean4/src/putnam_1997_b3.lean +++ b/lean4/src/putnam_1997_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Bornology Set diff --git a/lean4/src/putnam_1997_b4.lean b/lean4/src/putnam_1997_b4.lean index 0eac016f..6da26712 100644 --- a/lean4/src/putnam_1997_b4.lean +++ b/lean4/src/putnam_1997_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Bornology Set Polynomial diff --git a/lean4/src/putnam_1997_b5.lean b/lean4/src/putnam_1997_b5.lean index e4ff6421..de0f50b2 100644 --- a/lean4/src/putnam_1997_b5.lean +++ b/lean4/src/putnam_1997_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators def tetration : ℕ → ℕ → ℕ | _, 0 => 1 diff --git a/lean4/src/putnam_1998_a2.lean b/lean4/src/putnam_1998_a2.lean index c0aa8c11..2e32cc39 100644 --- a/lean4/src/putnam_1998_a2.lean +++ b/lean4/src/putnam_1998_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $s$ be any arc of the unit circle lying entirely in the first quadrant. Let $A$ be the area of the region lying below $s$ and above the $x$-axis and let $B$ be the area of the region lying to the right of the $y$-axis and to the left of $s$. Prove that $A+B$ depends only on the arc length, and not on the position, of $s$. diff --git a/lean4/src/putnam_1998_a3.lean b/lean4/src/putnam_1998_a3.lean index 0afd9b55..90d7e222 100644 --- a/lean4/src/putnam_1998_a3.lean +++ b/lean4/src/putnam_1998_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $f$ be a real function on the real line with continuous third derivative. Prove that there exists a point $a$ such that \[f(a)\cdot f'(a) \cdot f''(a) \cdot f'''(a)\geq 0 .\] diff --git a/lean4/src/putnam_1998_a4.lean b/lean4/src/putnam_1998_a4.lean index cf8a498b..73859754 100644 --- a/lean4/src/putnam_1998_a4.lean +++ b/lean4/src/putnam_1998_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators -- Note: Since 11 divides `x` iff it divides its base-10 reverse, the `reverse` below is optional. abbrev putnam_1998_a4_solution : Set ℕ := sorry diff --git a/lean4/src/putnam_1998_a5.lean b/lean4/src/putnam_1998_a5.lean index 24eaf852..228fd217 100644 --- a/lean4/src/putnam_1998_a5.lean +++ b/lean4/src/putnam_1998_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Metric diff --git a/lean4/src/putnam_1998_a6.lean b/lean4/src/putnam_1998_a6.lean index 9a75f868..8e00f017 100644 --- a/lean4/src/putnam_1998_a6.lean +++ b/lean4/src/putnam_1998_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Metric diff --git a/lean4/src/putnam_1998_b1.lean b/lean4/src/putnam_1998_b1.lean index e96f5fae..5e66d19c 100644 --- a/lean4/src/putnam_1998_b1.lean +++ b/lean4/src/putnam_1998_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Metric diff --git a/lean4/src/putnam_1998_b2.lean b/lean4/src/putnam_1998_b2.lean index 47576b28..3a3817c1 100644 --- a/lean4/src/putnam_1998_b2.lean +++ b/lean4/src/putnam_1998_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Metric diff --git a/lean4/src/putnam_1998_b4.lean b/lean4/src/putnam_1998_b4.lean index 15ad840b..582f1bde 100644 --- a/lean4/src/putnam_1998_b4.lean +++ b/lean4/src/putnam_1998_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Metric diff --git a/lean4/src/putnam_1998_b5.lean b/lean4/src/putnam_1998_b5.lean index eb438bcf..7f3c3caf 100644 --- a/lean4/src/putnam_1998_b5.lean +++ b/lean4/src/putnam_1998_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Metric diff --git a/lean4/src/putnam_1998_b6.lean b/lean4/src/putnam_1998_b6.lean index db0b507c..1b1600a1 100644 --- a/lean4/src/putnam_1998_b6.lean +++ b/lean4/src/putnam_1998_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Function Metric diff --git a/lean4/src/putnam_1999_a1.lean b/lean4/src/putnam_1999_a1.lean index f9404aec..e58b6fbf 100644 --- a/lean4/src/putnam_1999_a1.lean +++ b/lean4/src/putnam_1999_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators -- Note: The actual problem asks to "find" such polynomials as well - but the solution does not give a set of all possible solutions. Hence, we would need to do the analysis ourselves, the following formalization should work. abbrev putnam_1999_a1_solution : Prop := sorry diff --git a/lean4/src/putnam_1999_a2.lean b/lean4/src/putnam_1999_a2.lean index 2a31cc8b..87e99c21 100644 --- a/lean4/src/putnam_1999_a2.lean +++ b/lean4/src/putnam_1999_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $p(x)$ be a polynomial that is nonnegative for all real $x$. Prove that for some $k$, there are polynomials $f_1(x),\dots,f_k(x$) such that \[p(x) = \sum_{j=1}^k (f_j(x))^2.\] diff --git a/lean4/src/putnam_1999_a3.lean b/lean4/src/putnam_1999_a3.lean index ccaaa488..996eb8e5 100644 --- a/lean4/src/putnam_1999_a3.lean +++ b/lean4/src/putnam_1999_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_a4.lean b/lean4/src/putnam_1999_a4.lean index c67ec123..9b194508 100644 --- a/lean4/src/putnam_1999_a4.lean +++ b/lean4/src/putnam_1999_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_a5.lean b/lean4/src/putnam_1999_a5.lean index 57bf800f..4ff3acfd 100644 --- a/lean4/src/putnam_1999_a5.lean +++ b/lean4/src/putnam_1999_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_a6.lean b/lean4/src/putnam_1999_a6.lean index 178ef021..16ca1550 100644 --- a/lean4/src/putnam_1999_a6.lean +++ b/lean4/src/putnam_1999_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_b2.lean b/lean4/src/putnam_1999_b2.lean index 11ae0b52..6616a8d4 100644 --- a/lean4/src/putnam_1999_b2.lean +++ b/lean4/src/putnam_1999_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_b3.lean b/lean4/src/putnam_1999_b3.lean index f157ad24..3a51656c 100644 --- a/lean4/src/putnam_1999_b3.lean +++ b/lean4/src/putnam_1999_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_b4.lean b/lean4/src/putnam_1999_b4.lean index 67222cc9..985fb477 100644 --- a/lean4/src/putnam_1999_b4.lean +++ b/lean4/src/putnam_1999_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_b5.lean b/lean4/src/putnam_1999_b5.lean index a1f4f888..1f6668ff 100644 --- a/lean4/src/putnam_1999_b5.lean +++ b/lean4/src/putnam_1999_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_1999_b6.lean b/lean4/src/putnam_1999_b6.lean index d8c10f31..4316e537 100644 --- a/lean4/src/putnam_1999_b6.lean +++ b/lean4/src/putnam_1999_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_2000_a1.lean b/lean4/src/putnam_2000_a1.lean index 86df71ae..54262a53 100644 --- a/lean4/src/putnam_2000_a1.lean +++ b/lean4/src/putnam_2000_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2000_a2.lean b/lean4/src/putnam_2000_a2.lean index 3516eee1..f22022e5 100644 --- a/lean4/src/putnam_2000_a2.lean +++ b/lean4/src/putnam_2000_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2000_a4.lean b/lean4/src/putnam_2000_a4.lean index 2503722a..fb34c50a 100644 --- a/lean4/src/putnam_2000_a4.lean +++ b/lean4/src/putnam_2000_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2000_a5.lean b/lean4/src/putnam_2000_a5.lean index 4b8c8a0f..70b1277c 100644 --- a/lean4/src/putnam_2000_a5.lean +++ b/lean4/src/putnam_2000_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2000_a6.lean b/lean4/src/putnam_2000_a6.lean index 63eb01cb..7d28d393 100644 --- a/lean4/src/putnam_2000_a6.lean +++ b/lean4/src/putnam_2000_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2000_b1.lean b/lean4/src/putnam_2000_b1.lean index ef16aa34..ae8c194f 100644 --- a/lean4/src/putnam_2000_b1.lean +++ b/lean4/src/putnam_2000_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2000_b2.lean b/lean4/src/putnam_2000_b2.lean index ea55d24e..065e9733 100644 --- a/lean4/src/putnam_2000_b2.lean +++ b/lean4/src/putnam_2000_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2000_b3.lean b/lean4/src/putnam_2000_b3.lean index 9cd743d8..eee42412 100644 --- a/lean4/src/putnam_2000_b3.lean +++ b/lean4/src/putnam_2000_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Set Function diff --git a/lean4/src/putnam_2000_b4.lean b/lean4/src/putnam_2000_b4.lean index 57f29b7e..c34fed08 100644 --- a/lean4/src/putnam_2000_b4.lean +++ b/lean4/src/putnam_2000_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Set Function diff --git a/lean4/src/putnam_2000_b5.lean b/lean4/src/putnam_2000_b5.lean index 647389c3..c4c72258 100644 --- a/lean4/src/putnam_2000_b5.lean +++ b/lean4/src/putnam_2000_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Set Function diff --git a/lean4/src/putnam_2001_a1.lean b/lean4/src/putnam_2001_a1.lean index 69384fb8..bf646f63 100644 --- a/lean4/src/putnam_2001_a1.lean +++ b/lean4/src/putnam_2001_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2001_a3.lean b/lean4/src/putnam_2001_a3.lean index 9f5afa72..f8b49005 100644 --- a/lean4/src/putnam_2001_a3.lean +++ b/lean4/src/putnam_2001_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2001_a5.lean b/lean4/src/putnam_2001_a5.lean index d4ac9a1c..00a2ebc0 100644 --- a/lean4/src/putnam_2001_a5.lean +++ b/lean4/src/putnam_2001_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2001_b1.lean b/lean4/src/putnam_2001_b1.lean index 010568d1..add7046f 100644 --- a/lean4/src/putnam_2001_b1.lean +++ b/lean4/src/putnam_2001_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2001_b2.lean b/lean4/src/putnam_2001_b2.lean index 23bf1a6a..83352b32 100644 --- a/lean4/src/putnam_2001_b2.lean +++ b/lean4/src/putnam_2001_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2001_b3.lean b/lean4/src/putnam_2001_b3.lean index 89f1b339..5a09ea37 100644 --- a/lean4/src/putnam_2001_b3.lean +++ b/lean4/src/putnam_2001_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2001_b4.lean b/lean4/src/putnam_2001_b4.lean index e20a5d0c..5f211f56 100644 --- a/lean4/src/putnam_2001_b4.lean +++ b/lean4/src/putnam_2001_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2001_b5.lean b/lean4/src/putnam_2001_b5.lean index b89d2e1f..928cb3ec 100644 --- a/lean4/src/putnam_2001_b5.lean +++ b/lean4/src/putnam_2001_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2001_b6.lean b/lean4/src/putnam_2001_b6.lean index bf8dd68d..b62cb768 100644 --- a/lean4/src/putnam_2001_b6.lean +++ b/lean4/src/putnam_2001_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Polynomial Set diff --git a/lean4/src/putnam_2002_a1.lean b/lean4/src/putnam_2002_a1.lean index 50cc7d89..876cc094 100644 --- a/lean4/src/putnam_2002_a1.lean +++ b/lean4/src/putnam_2002_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2002_a2.lean b/lean4/src/putnam_2002_a2.lean index 8a0a317a..74bf1dd8 100644 --- a/lean4/src/putnam_2002_a2.lean +++ b/lean4/src/putnam_2002_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Metric diff --git a/lean4/src/putnam_2002_a3.lean b/lean4/src/putnam_2002_a3.lean index 13728a43..f4ba63fc 100644 --- a/lean4/src/putnam_2002_a3.lean +++ b/lean4/src/putnam_2002_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2002_a5.lean b/lean4/src/putnam_2002_a5.lean index cd7f2e79..09052242 100644 --- a/lean4/src/putnam_2002_a5.lean +++ b/lean4/src/putnam_2002_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2002_a6.lean b/lean4/src/putnam_2002_a6.lean index 875e1f23..a5c0bf06 100644 --- a/lean4/src/putnam_2002_a6.lean +++ b/lean4/src/putnam_2002_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set Topology Filter diff --git a/lean4/src/putnam_2002_b3.lean b/lean4/src/putnam_2002_b3.lean index ca6c9547..f3c13e9f 100644 --- a/lean4/src/putnam_2002_b3.lean +++ b/lean4/src/putnam_2002_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set Topology Filter diff --git a/lean4/src/putnam_2002_b5.lean b/lean4/src/putnam_2002_b5.lean index 46c196ff..93597241 100644 --- a/lean4/src/putnam_2002_b5.lean +++ b/lean4/src/putnam_2002_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set Topology Filter diff --git a/lean4/src/putnam_2002_b6.lean b/lean4/src/putnam_2002_b6.lean index 09d84c2c..e6e4049d 100644 --- a/lean4/src/putnam_2002_b6.lean +++ b/lean4/src/putnam_2002_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set Topology Filter Matrix MvPolynomial diff --git a/lean4/src/putnam_2003_a1.lean b/lean4/src/putnam_2003_a1.lean index 33bea4cb..2ddf5eec 100644 --- a/lean4/src/putnam_2003_a1.lean +++ b/lean4/src/putnam_2003_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial diff --git a/lean4/src/putnam_2003_a2.lean b/lean4/src/putnam_2003_a2.lean index fe66e933..d62d88d4 100644 --- a/lean4/src/putnam_2003_a2.lean +++ b/lean4/src/putnam_2003_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial diff --git a/lean4/src/putnam_2003_a3.lean b/lean4/src/putnam_2003_a3.lean index 13181842..8f7776fa 100644 --- a/lean4/src/putnam_2003_a3.lean +++ b/lean4/src/putnam_2003_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial diff --git a/lean4/src/putnam_2003_a4.lean b/lean4/src/putnam_2003_a4.lean index 6148a806..89aed5b4 100644 --- a/lean4/src/putnam_2003_a4.lean +++ b/lean4/src/putnam_2003_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial diff --git a/lean4/src/putnam_2003_a5.lean b/lean4/src/putnam_2003_a5.lean index a7a5a84a..f2fcef20 100644 --- a/lean4/src/putnam_2003_a5.lean +++ b/lean4/src/putnam_2003_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set diff --git a/lean4/src/putnam_2003_a6.lean b/lean4/src/putnam_2003_a6.lean index 2d7d7463..6432fa29 100644 --- a/lean4/src/putnam_2003_a6.lean +++ b/lean4/src/putnam_2003_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set diff --git a/lean4/src/putnam_2003_b1.lean b/lean4/src/putnam_2003_b1.lean index 9c75e09a..7b9afd71 100644 --- a/lean4/src/putnam_2003_b1.lean +++ b/lean4/src/putnam_2003_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set diff --git a/lean4/src/putnam_2003_b2.lean b/lean4/src/putnam_2003_b2.lean index af76c6f5..5aa07b1b 100644 --- a/lean4/src/putnam_2003_b2.lean +++ b/lean4/src/putnam_2003_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set diff --git a/lean4/src/putnam_2003_b3.lean b/lean4/src/putnam_2003_b3.lean index af1ef621..02232f47 100644 --- a/lean4/src/putnam_2003_b3.lean +++ b/lean4/src/putnam_2003_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set Nat diff --git a/lean4/src/putnam_2003_b4.lean b/lean4/src/putnam_2003_b4.lean index 1ec728a0..6caffa2c 100644 --- a/lean4/src/putnam_2003_b4.lean +++ b/lean4/src/putnam_2003_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set Nat diff --git a/lean4/src/putnam_2003_b5.lean b/lean4/src/putnam_2003_b5.lean index 5a0c159d..83a122e4 100644 --- a/lean4/src/putnam_2003_b5.lean +++ b/lean4/src/putnam_2003_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set Nat diff --git a/lean4/src/putnam_2003_b6.lean b/lean4/src/putnam_2003_b6.lean index 2e9119d4..cd97e0c3 100644 --- a/lean4/src/putnam_2003_b6.lean +++ b/lean4/src/putnam_2003_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MvPolynomial Set Nat diff --git a/lean4/src/putnam_2004_a1.lean b/lean4/src/putnam_2004_a1.lean index f56371ff..9d0fb180 100644 --- a/lean4/src/putnam_2004_a1.lean +++ b/lean4/src/putnam_2004_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_a3.lean b/lean4/src/putnam_2004_a3.lean index 18740e6f..742c5362 100644 --- a/lean4/src/putnam_2004_a3.lean +++ b/lean4/src/putnam_2004_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_a4.lean b/lean4/src/putnam_2004_a4.lean index 6a052716..e389f2b2 100644 --- a/lean4/src/putnam_2004_a4.lean +++ b/lean4/src/putnam_2004_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_a5.lean b/lean4/src/putnam_2004_a5.lean index bcc1c49d..01319309 100644 --- a/lean4/src/putnam_2004_a5.lean +++ b/lean4/src/putnam_2004_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_a6.lean b/lean4/src/putnam_2004_a6.lean index a44f00b6..76bc7154 100644 --- a/lean4/src/putnam_2004_a6.lean +++ b/lean4/src/putnam_2004_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_b1.lean b/lean4/src/putnam_2004_b1.lean index e3e5a544..aa2c88bf 100644 --- a/lean4/src/putnam_2004_b1.lean +++ b/lean4/src/putnam_2004_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_b2.lean b/lean4/src/putnam_2004_b2.lean index 86c1b6a3..49de50cf 100644 --- a/lean4/src/putnam_2004_b2.lean +++ b/lean4/src/putnam_2004_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_b4.lean b/lean4/src/putnam_2004_b4.lean index a0e00859..c22a8656 100644 --- a/lean4/src/putnam_2004_b4.lean +++ b/lean4/src/putnam_2004_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_b5.lean b/lean4/src/putnam_2004_b5.lean index 7ce119cd..cedef415 100644 --- a/lean4/src/putnam_2004_b5.lean +++ b/lean4/src/putnam_2004_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2004_b6.lean b/lean4/src/putnam_2004_b6.lean index dbf5f9f8..e23032b6 100644 --- a/lean4/src/putnam_2004_b6.lean +++ b/lean4/src/putnam_2004_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2005_a1.lean b/lean4/src/putnam_2005_a1.lean index ebdee0fd..db848fb0 100644 --- a/lean4/src/putnam_2005_a1.lean +++ b/lean4/src/putnam_2005_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2005_a2.lean b/lean4/src/putnam_2005_a2.lean index d34c3a89..328d0216 100644 --- a/lean4/src/putnam_2005_a2.lean +++ b/lean4/src/putnam_2005_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_a3.lean b/lean4/src/putnam_2005_a3.lean index 6587a7ef..fe3d46f4 100644 --- a/lean4/src/putnam_2005_a3.lean +++ b/lean4/src/putnam_2005_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_a4.lean b/lean4/src/putnam_2005_a4.lean index 092cb8c6..2ed7a878 100644 --- a/lean4/src/putnam_2005_a4.lean +++ b/lean4/src/putnam_2005_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_a5.lean b/lean4/src/putnam_2005_a5.lean index f9a7fbb5..64aa9ce0 100644 --- a/lean4/src/putnam_2005_a5.lean +++ b/lean4/src/putnam_2005_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_b1.lean b/lean4/src/putnam_2005_b1.lean index 13311edd..f79ddbae 100644 --- a/lean4/src/putnam_2005_b1.lean +++ b/lean4/src/putnam_2005_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_b2.lean b/lean4/src/putnam_2005_b2.lean index 6d1f6558..e8c0bcbd 100644 --- a/lean4/src/putnam_2005_b2.lean +++ b/lean4/src/putnam_2005_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_b3.lean b/lean4/src/putnam_2005_b3.lean index 6b968603..19cfec9a 100644 --- a/lean4/src/putnam_2005_b3.lean +++ b/lean4/src/putnam_2005_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_b4.lean b/lean4/src/putnam_2005_b4.lean index d601748f..58df69bd 100644 --- a/lean4/src/putnam_2005_b4.lean +++ b/lean4/src/putnam_2005_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_b5.lean b/lean4/src/putnam_2005_b5.lean index 4e3e86e4..038ea657 100644 --- a/lean4/src/putnam_2005_b5.lean +++ b/lean4/src/putnam_2005_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2005_b6.lean b/lean4/src/putnam_2005_b6.lean index cbfd5e88..f29c8dbf 100644 --- a/lean4/src/putnam_2005_b6.lean +++ b/lean4/src/putnam_2005_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Set diff --git a/lean4/src/putnam_2006_a1.lean b/lean4/src/putnam_2006_a1.lean index 9f1eb76b..d33f9d94 100644 --- a/lean4/src/putnam_2006_a1.lean +++ b/lean4/src/putnam_2006_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_2006_a1_solution : ℝ := sorry -- 6 * Real.pi ^ 2 diff --git a/lean4/src/putnam_2006_a3.lean b/lean4/src/putnam_2006_a3.lean index 5688da0e..9cce7951 100644 --- a/lean4/src/putnam_2006_a3.lean +++ b/lean4/src/putnam_2006_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $1, 2, 3, \dots, 2005, 2006, 2007, 2009, 2012, 2016, \dots$ be a sequence defined by $x_k = k$ for $k=1, 2, \dots, 2006$ and $x_{k+1} = x_k + x_{k-2005}$ for $k \geq 2006$. Show that the sequence has $2005$ consecutive terms each divisible by $2006$. diff --git a/lean4/src/putnam_2006_a4.lean b/lean4/src/putnam_2006_a4.lean index 5fff1d40..b1c6d33c 100644 --- a/lean4/src/putnam_2006_a4.lean +++ b/lean4/src/putnam_2006_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators -- Note: uses (ℕ → ℕ) instead of (Equiv.Perm (Fin n)) noncomputable abbrev putnam_2006_a4_solution : ℕ → ℝ := sorry diff --git a/lean4/src/putnam_2006_a5.lean b/lean4/src/putnam_2006_a5.lean index e1698f64..9b295188 100644 --- a/lean4/src/putnam_2006_a5.lean +++ b/lean4/src/putnam_2006_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2006_a5_solution : ℕ → ℤ := sorry -- (fun n : ℕ => if (n ≡ 1 [MOD 4]) then n else -n) diff --git a/lean4/src/putnam_2006_b1.lean b/lean4/src/putnam_2006_b1.lean index 5216da35..04fccb5e 100644 --- a/lean4/src/putnam_2006_b1.lean +++ b/lean4/src/putnam_2006_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_2006_b1_solution : ℝ := sorry -- 3 * Real.sqrt 3 / 2 diff --git a/lean4/src/putnam_2006_b2.lean b/lean4/src/putnam_2006_b2.lean index bdea7615..91b745e3 100644 --- a/lean4/src/putnam_2006_b2.lean +++ b/lean4/src/putnam_2006_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Prove that, for every set $X = \{x_1, x_2, \dots, x_n\}$ of $n$ real numbers, there exists a non-empty subset $S$ of $X$ and an integer $m$ such that diff --git a/lean4/src/putnam_2006_b3.lean b/lean4/src/putnam_2006_b3.lean index 0a083087..d192c362 100644 --- a/lean4/src/putnam_2006_b3.lean +++ b/lean4/src/putnam_2006_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2006_b3_solution : ℕ → ℕ := sorry -- (fun n : ℕ => (Nat.choose n 2) + 1) diff --git a/lean4/src/putnam_2006_b4.lean b/lean4/src/putnam_2006_b4.lean index dd44dc10..a2c374e6 100644 --- a/lean4/src/putnam_2006_b4.lean +++ b/lean4/src/putnam_2006_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_2006_b4_solution : ℕ → ℕ := sorry -- fun k ↦ 2 ^ k diff --git a/lean4/src/putnam_2006_b5.lean b/lean4/src/putnam_2006_b5.lean index f117a7ca..06c6a316 100644 --- a/lean4/src/putnam_2006_b5.lean +++ b/lean4/src/putnam_2006_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set diff --git a/lean4/src/putnam_2006_b6.lean b/lean4/src/putnam_2006_b6.lean index 873bbfea..c80a69d8 100644 --- a/lean4/src/putnam_2006_b6.lean +++ b/lean4/src/putnam_2006_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Topology Filter diff --git a/lean4/src/putnam_2007_a1.lean b/lean4/src/putnam_2007_a1.lean index 7a620699..c68657d5 100644 --- a/lean4/src/putnam_2007_a1.lean +++ b/lean4/src/putnam_2007_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2007_a1_solution : Set ℝ := sorry -- {2 / 3, 3 / 2, (13 + √601) / 12, (13 - √601) / 12} diff --git a/lean4/src/putnam_2007_a2.lean b/lean4/src/putnam_2007_a2.lean index 36813495..77c634f4 100644 --- a/lean4/src/putnam_2007_a2.lean +++ b/lean4/src/putnam_2007_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_2007_a2_solution : ENNReal := sorry -- 4 diff --git a/lean4/src/putnam_2007_a3.lean b/lean4/src/putnam_2007_a3.lean index 1a494806..1882dee9 100644 --- a/lean4/src/putnam_2007_a3.lean +++ b/lean4/src/putnam_2007_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set open scoped Nat diff --git a/lean4/src/putnam_2007_a4.lean b/lean4/src/putnam_2007_a4.lean index 360451a2..10b77c9f 100644 --- a/lean4/src/putnam_2007_a4.lean +++ b/lean4/src/putnam_2007_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat diff --git a/lean4/src/putnam_2007_a5.lean b/lean4/src/putnam_2007_a5.lean index ecf5c3bf..0f56ca56 100644 --- a/lean4/src/putnam_2007_a5.lean +++ b/lean4/src/putnam_2007_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat diff --git a/lean4/src/putnam_2007_b1.lean b/lean4/src/putnam_2007_b1.lean index f408626e..79dfa49a 100644 --- a/lean4/src/putnam_2007_b1.lean +++ b/lean4/src/putnam_2007_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat diff --git a/lean4/src/putnam_2007_b2.lean b/lean4/src/putnam_2007_b2.lean index 764359c1..0c012fbf 100644 --- a/lean4/src/putnam_2007_b2.lean +++ b/lean4/src/putnam_2007_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Function diff --git a/lean4/src/putnam_2007_b3.lean b/lean4/src/putnam_2007_b3.lean index 9d4efe2b..1b30c259 100644 --- a/lean4/src/putnam_2007_b3.lean +++ b/lean4/src/putnam_2007_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Function diff --git a/lean4/src/putnam_2007_b4.lean b/lean4/src/putnam_2007_b4.lean index 68d4d671..2b6b1604 100644 --- a/lean4/src/putnam_2007_b4.lean +++ b/lean4/src/putnam_2007_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Function diff --git a/lean4/src/putnam_2007_b5.lean b/lean4/src/putnam_2007_b5.lean index 85af96aa..22ce05b4 100644 --- a/lean4/src/putnam_2007_b5.lean +++ b/lean4/src/putnam_2007_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Function diff --git a/lean4/src/putnam_2007_b6.lean b/lean4/src/putnam_2007_b6.lean index 7e00d7c2..b4439de3 100644 --- a/lean4/src/putnam_2007_b6.lean +++ b/lean4/src/putnam_2007_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Set Nat Function diff --git a/lean4/src/putnam_2008_a1.lean b/lean4/src/putnam_2008_a1.lean index a432a71c..f269d23e 100644 --- a/lean4/src/putnam_2008_a1.lean +++ b/lean4/src/putnam_2008_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $f:\mathbb{R}^2 \to \mathbb{R}$ be a function such that $f(x,y)+f(y,z)+f(z,x)=0$ for all real numbers $x$, $y$, and $z$. Prove that there exists a function $g:\mathbb{R} \to \mathbb{R}$ such that $f(x,y)=g(x)-g(y)$ for all real numbers $x$ and $y$. diff --git a/lean4/src/putnam_2008_a3.lean b/lean4/src/putnam_2008_a3.lean index 174fe30b..a5a2df78 100644 --- a/lean4/src/putnam_2008_a3.lean +++ b/lean4/src/putnam_2008_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Start with a finite sequence $a_1, a_2, \dots, a_n$ of positive integers. If possible, choose two indices $j < k$ such that $a_j$ does not divide $a_k$, and replace $a_j$ and $a_k$ by $\mathrm{gcd}(a_j, a_k)$ and $\mathrm{lcm}(a_j, a_k)$, respectively. Prove that if this process is repeated, it must eventually stop and the final sequence does not depend on the choices made. diff --git a/lean4/src/putnam_2008_a4.lean b/lean4/src/putnam_2008_a4.lean index c2ce696b..da0f3d2b 100644 --- a/lean4/src/putnam_2008_a4.lean +++ b/lean4/src/putnam_2008_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2008_a5.lean b/lean4/src/putnam_2008_a5.lean index 6c964a69..d15c3433 100644 --- a/lean4/src/putnam_2008_a5.lean +++ b/lean4/src/putnam_2008_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2008_a6.lean b/lean4/src/putnam_2008_a6.lean index 697a999a..72ea9df1 100644 --- a/lean4/src/putnam_2008_a6.lean +++ b/lean4/src/putnam_2008_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2008_b1.lean b/lean4/src/putnam_2008_b1.lean index 7cbfade5..c7bde71b 100644 --- a/lean4/src/putnam_2008_b1.lean +++ b/lean4/src/putnam_2008_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2008_b2.lean b/lean4/src/putnam_2008_b2.lean index b26ccf7e..e40c1b95 100644 --- a/lean4/src/putnam_2008_b2.lean +++ b/lean4/src/putnam_2008_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set Nat diff --git a/lean4/src/putnam_2008_b3.lean b/lean4/src/putnam_2008_b3.lean index e89b0ce0..902ac7f4 100644 --- a/lean4/src/putnam_2008_b3.lean +++ b/lean4/src/putnam_2008_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open FiniteDimensional Metric Filter Topology Set Nat diff --git a/lean4/src/putnam_2008_b4.lean b/lean4/src/putnam_2008_b4.lean index d772a3e1..24f29354 100644 --- a/lean4/src/putnam_2008_b4.lean +++ b/lean4/src/putnam_2008_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set Nat diff --git a/lean4/src/putnam_2008_b5.lean b/lean4/src/putnam_2008_b5.lean index 73683741..edb14275 100644 --- a/lean4/src/putnam_2008_b5.lean +++ b/lean4/src/putnam_2008_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set Nat diff --git a/lean4/src/putnam_2008_b6.lean b/lean4/src/putnam_2008_b6.lean index 9c241a86..5c29fbf8 100644 --- a/lean4/src/putnam_2008_b6.lean +++ b/lean4/src/putnam_2008_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set Nat diff --git a/lean4/src/putnam_2009_a1.lean b/lean4/src/putnam_2009_a1.lean index 76c3d107..247d26ad 100644 --- a/lean4/src/putnam_2009_a1.lean +++ b/lean4/src/putnam_2009_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter diff --git a/lean4/src/putnam_2009_a2.lean b/lean4/src/putnam_2009_a2.lean index 3e5bfb74..40ddd638 100644 --- a/lean4/src/putnam_2009_a2.lean +++ b/lean4/src/putnam_2009_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set diff --git a/lean4/src/putnam_2009_a3.lean b/lean4/src/putnam_2009_a3.lean index dfb80b89..3696a3df 100644 --- a/lean4/src/putnam_2009_a3.lean +++ b/lean4/src/putnam_2009_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set diff --git a/lean4/src/putnam_2009_a4.lean b/lean4/src/putnam_2009_a4.lean index 36581d02..b147901e 100644 --- a/lean4/src/putnam_2009_a4.lean +++ b/lean4/src/putnam_2009_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set diff --git a/lean4/src/putnam_2009_a5.lean b/lean4/src/putnam_2009_a5.lean index b6fb9fee..a5fdaa4d 100644 --- a/lean4/src/putnam_2009_a5.lean +++ b/lean4/src/putnam_2009_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set diff --git a/lean4/src/putnam_2009_b1.lean b/lean4/src/putnam_2009_b1.lean index dd2380de..09a54fb4 100644 --- a/lean4/src/putnam_2009_b1.lean +++ b/lean4/src/putnam_2009_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set diff --git a/lean4/src/putnam_2009_b2.lean b/lean4/src/putnam_2009_b2.lean index 3d58e24b..c72d8a26 100644 --- a/lean4/src/putnam_2009_b2.lean +++ b/lean4/src/putnam_2009_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set diff --git a/lean4/src/putnam_2009_b3.lean b/lean4/src/putnam_2009_b3.lean index 4e2b2499..b7495152 100644 --- a/lean4/src/putnam_2009_b3.lean +++ b/lean4/src/putnam_2009_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set diff --git a/lean4/src/putnam_2009_b4.lean b/lean4/src/putnam_2009_b4.lean index 6cd3149b..4cd7bea2 100644 --- a/lean4/src/putnam_2009_b4.lean +++ b/lean4/src/putnam_2009_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set Metric diff --git a/lean4/src/putnam_2009_b5.lean b/lean4/src/putnam_2009_b5.lean index 7abef72e..e7e743e0 100644 --- a/lean4/src/putnam_2009_b5.lean +++ b/lean4/src/putnam_2009_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set Metric diff --git a/lean4/src/putnam_2009_b6.lean b/lean4/src/putnam_2009_b6.lean index c54c3940..995296d5 100644 --- a/lean4/src/putnam_2009_b6.lean +++ b/lean4/src/putnam_2009_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology MvPolynomial Filter Set Metric diff --git a/lean4/src/putnam_2010_a1.lean b/lean4/src/putnam_2010_a1.lean index 35136472..4576e59d 100644 --- a/lean4/src/putnam_2010_a1.lean +++ b/lean4/src/putnam_2010_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_2010_a1_solution : ℕ → ℕ := sorry -- (fun n : ℕ => Nat.ceil ((n : ℝ) / 2)) diff --git a/lean4/src/putnam_2010_a2.lean b/lean4/src/putnam_2010_a2.lean index d2b692e1..348e73dd 100644 --- a/lean4/src/putnam_2010_a2.lean +++ b/lean4/src/putnam_2010_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2010_a2_solution : Set (ℝ → ℝ) := sorry -- {f : ℝ → ℝ | ∃ c d : ℝ, ∀ x : ℝ, f x = c*x + d} diff --git a/lean4/src/putnam_2010_a4.lean b/lean4/src/putnam_2010_a4.lean index c5d54c6d..a508d807 100644 --- a/lean4/src/putnam_2010_a4.lean +++ b/lean4/src/putnam_2010_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Prove that for each positive integer $n$, the number $10^{10^{10^n}} + 10^{10^n} + 10^n - 1$ is not prime. diff --git a/lean4/src/putnam_2010_a5.lean b/lean4/src/putnam_2010_a5.lean index 402aa82b..4879a369 100644 --- a/lean4/src/putnam_2010_a5.lean +++ b/lean4/src/putnam_2010_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $G$ be a group, with operation $*$. Suppose that \begin{enumerate} \item[(i)] $G$ is a subset of $\mathbb{R}^3$ (but $*$ need not be related to addition of vectors); \item[(ii)] For each $\mathbf{a},\mathbf{b} \in G$, either $\mathbf{a}\times \mathbf{b} = \mathbf{a}*\mathbf{b}$ or $\mathbf{a}\times \mathbf{b} = 0$ (or both), where $\times$ is the usual cross product in $\mathbb{R}^3$. \end{enumerate} Prove that $\mathbf{a} \times \mathbf{b} = 0$ for all $\mathbf{a}, \mathbf{b} \in G$. diff --git a/lean4/src/putnam_2010_a6.lean b/lean4/src/putnam_2010_a6.lean index fbbcb95e..657b3b23 100644 --- a/lean4/src/putnam_2010_a6.lean +++ b/lean4/src/putnam_2010_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2010_b1.lean b/lean4/src/putnam_2010_b1.lean index 7c374f0e..f74c268f 100644 --- a/lean4/src/putnam_2010_b1.lean +++ b/lean4/src/putnam_2010_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2010_b2.lean b/lean4/src/putnam_2010_b2.lean index cd598cee..c230b92a 100644 --- a/lean4/src/putnam_2010_b2.lean +++ b/lean4/src/putnam_2010_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set abbrev putnam_2010_b2_solution : ℕ := sorry diff --git a/lean4/src/putnam_2010_b3.lean b/lean4/src/putnam_2010_b3.lean index 870a4918..72158cb2 100644 --- a/lean4/src/putnam_2010_b3.lean +++ b/lean4/src/putnam_2010_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2010_b4.lean b/lean4/src/putnam_2010_b4.lean index 50511cf2..aef4599d 100644 --- a/lean4/src/putnam_2010_b4.lean +++ b/lean4/src/putnam_2010_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2010_b5.lean b/lean4/src/putnam_2010_b5.lean index 15cd70b5..d5d6f266 100644 --- a/lean4/src/putnam_2010_b5.lean +++ b/lean4/src/putnam_2010_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2010_b6.lean b/lean4/src/putnam_2010_b6.lean index fd0395cb..0830566c 100644 --- a/lean4/src/putnam_2010_b6.lean +++ b/lean4/src/putnam_2010_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2011_a1.lean b/lean4/src/putnam_2011_a1.lean index 1e08c572..f7ed031d 100644 --- a/lean4/src/putnam_2011_a1.lean +++ b/lean4/src/putnam_2011_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2011_a1_solution : ℕ := sorry -- 10053 diff --git a/lean4/src/putnam_2011_a2.lean b/lean4/src/putnam_2011_a2.lean index 57c0056d..fe64865a 100644 --- a/lean4/src/putnam_2011_a2.lean +++ b/lean4/src/putnam_2011_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2011_a3.lean b/lean4/src/putnam_2011_a3.lean index afa255e7..ac74524b 100644 --- a/lean4/src/putnam_2011_a3.lean +++ b/lean4/src/putnam_2011_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2011_a4.lean b/lean4/src/putnam_2011_a4.lean index 55efdb59..784c592d 100644 --- a/lean4/src/putnam_2011_a4.lean +++ b/lean4/src/putnam_2011_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_a5.lean b/lean4/src/putnam_2011_a5.lean index d8f3718c..6151a615 100644 --- a/lean4/src/putnam_2011_a5.lean +++ b/lean4/src/putnam_2011_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_a6.lean b/lean4/src/putnam_2011_a6.lean index c4081d07..60bf590f 100644 --- a/lean4/src/putnam_2011_a6.lean +++ b/lean4/src/putnam_2011_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_b1.lean b/lean4/src/putnam_2011_b1.lean index 5b797cdd..081c5fd1 100644 --- a/lean4/src/putnam_2011_b1.lean +++ b/lean4/src/putnam_2011_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_b2.lean b/lean4/src/putnam_2011_b2.lean index 50ae281e..711bfa70 100644 --- a/lean4/src/putnam_2011_b2.lean +++ b/lean4/src/putnam_2011_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_b3.lean b/lean4/src/putnam_2011_b3.lean index 2e0be997..22e94b52 100644 --- a/lean4/src/putnam_2011_b3.lean +++ b/lean4/src/putnam_2011_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_b4.lean b/lean4/src/putnam_2011_b4.lean index de848de9..3bfdc222 100644 --- a/lean4/src/putnam_2011_b4.lean +++ b/lean4/src/putnam_2011_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_b5.lean b/lean4/src/putnam_2011_b5.lean index 25db93e5..6dd47c93 100644 --- a/lean4/src/putnam_2011_b5.lean +++ b/lean4/src/putnam_2011_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix diff --git a/lean4/src/putnam_2011_b6.lean b/lean4/src/putnam_2011_b6.lean index 7c79d24d..fdb4667f 100644 --- a/lean4/src/putnam_2011_b6.lean +++ b/lean4/src/putnam_2011_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Matrix Set diff --git a/lean4/src/putnam_2012_a1.lean b/lean4/src/putnam_2012_a1.lean index e665f276..0c48a46b 100644 --- a/lean4/src/putnam_2012_a1.lean +++ b/lean4/src/putnam_2012_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix diff --git a/lean4/src/putnam_2012_a2.lean b/lean4/src/putnam_2012_a2.lean index e8f68935..7e138c70 100644 --- a/lean4/src/putnam_2012_a2.lean +++ b/lean4/src/putnam_2012_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix diff --git a/lean4/src/putnam_2012_a3.lean b/lean4/src/putnam_2012_a3.lean index 964271fb..59d6cb8d 100644 --- a/lean4/src/putnam_2012_a3.lean +++ b/lean4/src/putnam_2012_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function diff --git a/lean4/src/putnam_2012_a4.lean b/lean4/src/putnam_2012_a4.lean index ba80abcc..8a9a6c61 100644 --- a/lean4/src/putnam_2012_a4.lean +++ b/lean4/src/putnam_2012_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function diff --git a/lean4/src/putnam_2012_a5.lean b/lean4/src/putnam_2012_a5.lean index 75c1f5d2..8c20607b 100644 --- a/lean4/src/putnam_2012_a5.lean +++ b/lean4/src/putnam_2012_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function diff --git a/lean4/src/putnam_2012_a6.lean b/lean4/src/putnam_2012_a6.lean index 3493a95b..ee9cdfe2 100644 --- a/lean4/src/putnam_2012_a6.lean +++ b/lean4/src/putnam_2012_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function diff --git a/lean4/src/putnam_2012_b1.lean b/lean4/src/putnam_2012_b1.lean index e683a36e..b874ed3d 100644 --- a/lean4/src/putnam_2012_b1.lean +++ b/lean4/src/putnam_2012_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function Real diff --git a/lean4/src/putnam_2012_b3.lean b/lean4/src/putnam_2012_b3.lean index 04236afd..21a610dc 100644 --- a/lean4/src/putnam_2012_b3.lean +++ b/lean4/src/putnam_2012_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function Real diff --git a/lean4/src/putnam_2012_b4.lean b/lean4/src/putnam_2012_b4.lean index a9772c8c..e68ead34 100644 --- a/lean4/src/putnam_2012_b4.lean +++ b/lean4/src/putnam_2012_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function Real Topology Filter diff --git a/lean4/src/putnam_2012_b5.lean b/lean4/src/putnam_2012_b5.lean index a44011e7..d547115b 100644 --- a/lean4/src/putnam_2012_b5.lean +++ b/lean4/src/putnam_2012_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function Real Topology Filter diff --git a/lean4/src/putnam_2012_b6.lean b/lean4/src/putnam_2012_b6.lean index 4f6e66cf..eb49be2b 100644 --- a/lean4/src/putnam_2012_b6.lean +++ b/lean4/src/putnam_2012_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Matrix Function Real Topology Filter diff --git a/lean4/src/putnam_2013_a2.lean b/lean4/src/putnam_2013_a2.lean index 5271955a..42d81197 100644 --- a/lean4/src/putnam_2013_a2.lean +++ b/lean4/src/putnam_2013_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_a3.lean b/lean4/src/putnam_2013_a3.lean index 17f5c4a0..2356f362 100644 --- a/lean4/src/putnam_2013_a3.lean +++ b/lean4/src/putnam_2013_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_a4.lean b/lean4/src/putnam_2013_a4.lean index 2efe99f7..3867ce57 100644 --- a/lean4/src/putnam_2013_a4.lean +++ b/lean4/src/putnam_2013_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_a5.lean b/lean4/src/putnam_2013_a5.lean index dea90c93..e3d2baad 100644 --- a/lean4/src/putnam_2013_a5.lean +++ b/lean4/src/putnam_2013_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set MeasureTheory diff --git a/lean4/src/putnam_2013_a6.lean b/lean4/src/putnam_2013_a6.lean index b2cfa092..22135108 100644 --- a/lean4/src/putnam_2013_a6.lean +++ b/lean4/src/putnam_2013_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_b1.lean b/lean4/src/putnam_2013_b1.lean index 2a5baf51..28ccc648 100644 --- a/lean4/src/putnam_2013_b1.lean +++ b/lean4/src/putnam_2013_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_b2.lean b/lean4/src/putnam_2013_b2.lean index fd8b9146..f51eff3a 100644 --- a/lean4/src/putnam_2013_b2.lean +++ b/lean4/src/putnam_2013_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_b3.lean b/lean4/src/putnam_2013_b3.lean index e9825eaa..1c91246a 100644 --- a/lean4/src/putnam_2013_b3.lean +++ b/lean4/src/putnam_2013_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_b4.lean b/lean4/src/putnam_2013_b4.lean index 962be9d2..a8d09e8e 100644 --- a/lean4/src/putnam_2013_b4.lean +++ b/lean4/src/putnam_2013_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2013_b5.lean b/lean4/src/putnam_2013_b5.lean index 3739b787..3b07ae19 100644 --- a/lean4/src/putnam_2013_b5.lean +++ b/lean4/src/putnam_2013_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function Set diff --git a/lean4/src/putnam_2014_a1.lean b/lean4/src/putnam_2014_a1.lean index b0701ad8..5e5fcf51 100644 --- a/lean4/src/putnam_2014_a1.lean +++ b/lean4/src/putnam_2014_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2014_a2.lean b/lean4/src/putnam_2014_a2.lean index 3342f703..4e602a3d 100644 --- a/lean4/src/putnam_2014_a2.lean +++ b/lean4/src/putnam_2014_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_a3.lean b/lean4/src/putnam_2014_a3.lean index b3a9d793..2d75878f 100644 --- a/lean4/src/putnam_2014_a3.lean +++ b/lean4/src/putnam_2014_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_a4.lean b/lean4/src/putnam_2014_a4.lean index 368ced5e..3b07e1f0 100644 --- a/lean4/src/putnam_2014_a4.lean +++ b/lean4/src/putnam_2014_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_a5.lean b/lean4/src/putnam_2014_a5.lean index 817a013e..5dfb298a 100644 --- a/lean4/src/putnam_2014_a5.lean +++ b/lean4/src/putnam_2014_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_a6.lean b/lean4/src/putnam_2014_a6.lean index c93d7857..84936e7e 100644 --- a/lean4/src/putnam_2014_a6.lean +++ b/lean4/src/putnam_2014_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_b1.lean b/lean4/src/putnam_2014_b1.lean index b702dbab..6fb200a4 100644 --- a/lean4/src/putnam_2014_b1.lean +++ b/lean4/src/putnam_2014_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_b2.lean b/lean4/src/putnam_2014_b2.lean index 41171b06..4ae0bd72 100644 --- a/lean4/src/putnam_2014_b2.lean +++ b/lean4/src/putnam_2014_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_b3.lean b/lean4/src/putnam_2014_b3.lean index 11bb2d98..bccddf9e 100644 --- a/lean4/src/putnam_2014_b3.lean +++ b/lean4/src/putnam_2014_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_b4.lean b/lean4/src/putnam_2014_b4.lean index e8bbd509..e6803f61 100644 --- a/lean4/src/putnam_2014_b4.lean +++ b/lean4/src/putnam_2014_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat diff --git a/lean4/src/putnam_2014_b6.lean b/lean4/src/putnam_2014_b6.lean index 8790f808..96d838eb 100644 --- a/lean4/src/putnam_2014_b6.lean +++ b/lean4/src/putnam_2014_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Nat Set Interval diff --git a/lean4/src/putnam_2015_a1.lean b/lean4/src/putnam_2015_a1.lean index 4ee69f59..039d283c 100644 --- a/lean4/src/putnam_2015_a1.lean +++ b/lean4/src/putnam_2015_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $A$ and $B$ be points on the same branch of the hyperbola $xy=1$. Suppose that $P$ is a point lying between $A$ and $B$ on this hyperbola, such that the area of the triangle $APB$ is as large as possible. Show that the region bounded by the hyperbola and the chord $AP$ has the same area as the region bounded by the hyperbola and the chord $PB$. diff --git a/lean4/src/putnam_2015_a2.lean b/lean4/src/putnam_2015_a2.lean index 189b3d8c..4039c655 100644 --- a/lean4/src/putnam_2015_a2.lean +++ b/lean4/src/putnam_2015_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators -- Note: this problem admits several possible correct solutions; this is the one shown on the solutions document abbrev putnam_2015_a2_solution : ℕ := sorry diff --git a/lean4/src/putnam_2015_a3.lean b/lean4/src/putnam_2015_a3.lean index cb8406cc..d0e47392 100644 --- a/lean4/src/putnam_2015_a3.lean +++ b/lean4/src/putnam_2015_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2015_a3_solution : ℂ := sorry -- 13725 diff --git a/lean4/src/putnam_2015_a4.lean b/lean4/src/putnam_2015_a4.lean index f81dcfbb..939ed0a0 100644 --- a/lean4/src/putnam_2015_a4.lean +++ b/lean4/src/putnam_2015_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_2015_a4_solution : ℝ := sorry -- 4 / 7 diff --git a/lean4/src/putnam_2015_a5.lean b/lean4/src/putnam_2015_a5.lean index 95187b96..60928dea 100644 --- a/lean4/src/putnam_2015_a5.lean +++ b/lean4/src/putnam_2015_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $q$ be an odd positive integer, and let $N_q$ denote the number of integers $a$ such that $0 0 ∧ (x = 1 ∨ 5 ∣ x)} diff --git a/lean4/src/putnam_2017_a2.lean b/lean4/src/putnam_2017_a2.lean index 519eeef8..ec3b697b 100644 --- a/lean4/src/putnam_2017_a2.lean +++ b/lean4/src/putnam_2017_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $Q_0(x)=1$, $Q_1(x)=x$, and $Q_n(x)=\frac{(Q_{n-1}(x))^2-1}{Q_{n-2}(x)}$ for all $n \geq 2$. Show that, whenever $n$ is a positive integer, $Q_n(x)$ is equal to a polynomial with integer coefficients. diff --git a/lean4/src/putnam_2017_a3.lean b/lean4/src/putnam_2017_a3.lean index 3f230771..0d1c0260 100644 --- a/lean4/src/putnam_2017_a3.lean +++ b/lean4/src/putnam_2017_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2017_a4.lean b/lean4/src/putnam_2017_a4.lean index d5e9d426..5118fbb8 100644 --- a/lean4/src/putnam_2017_a4.lean +++ b/lean4/src/putnam_2017_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2017_b1.lean b/lean4/src/putnam_2017_b1.lean index 5944f47a..f2c7e4b3 100644 --- a/lean4/src/putnam_2017_b1.lean +++ b/lean4/src/putnam_2017_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2017_b2.lean b/lean4/src/putnam_2017_b2.lean index 4e78d88a..6db27c47 100644 --- a/lean4/src/putnam_2017_b2.lean +++ b/lean4/src/putnam_2017_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2017_b3.lean b/lean4/src/putnam_2017_b3.lean index 38ad6a48..77d3c104 100644 --- a/lean4/src/putnam_2017_b3.lean +++ b/lean4/src/putnam_2017_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2017_b4.lean b/lean4/src/putnam_2017_b4.lean index 625cafbf..10b29d31 100644 --- a/lean4/src/putnam_2017_b4.lean +++ b/lean4/src/putnam_2017_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Real diff --git a/lean4/src/putnam_2017_b6.lean b/lean4/src/putnam_2017_b6.lean index 024368fe..d1cc2a9c 100644 --- a/lean4/src/putnam_2017_b6.lean +++ b/lean4/src/putnam_2017_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Real Function Nat diff --git a/lean4/src/putnam_2018_a1.lean b/lean4/src/putnam_2018_a1.lean index b4e91dfb..109f3b08 100644 --- a/lean4/src/putnam_2018_a1.lean +++ b/lean4/src/putnam_2018_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2018_a1_solution : Set (ℤ × ℤ) := sorry -- {⟨673, 1358114⟩, ⟨674, 340033⟩, ⟨1009, 2018⟩, ⟨2018, 1009⟩, ⟨340033, 674⟩, ⟨1358114, 673⟩} diff --git a/lean4/src/putnam_2018_a2.lean b/lean4/src/putnam_2018_a2.lean index 42694918..4ca787b9 100644 --- a/lean4/src/putnam_2018_a2.lean +++ b/lean4/src/putnam_2018_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2018_a2_solution : ℕ → ℝ := sorry -- (fun n : ℕ => if n = 1 then 1 else -1) diff --git a/lean4/src/putnam_2018_a3.lean b/lean4/src/putnam_2018_a3.lean index 526b5df0..82ed0275 100644 --- a/lean4/src/putnam_2018_a3.lean +++ b/lean4/src/putnam_2018_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators noncomputable abbrev putnam_2018_a3_solution : ℝ := sorry -- 480/49 diff --git a/lean4/src/putnam_2018_a4.lean b/lean4/src/putnam_2018_a4.lean index c9ea07db..7963a974 100644 --- a/lean4/src/putnam_2018_a4.lean +++ b/lean4/src/putnam_2018_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators -- Note: uses (ℕ → ℕ) instead of (Set.Icc 1 n → ℕ) /-- diff --git a/lean4/src/putnam_2018_a5.lean b/lean4/src/putnam_2018_a5.lean index 88ed079c..c393fcc8 100644 --- a/lean4/src/putnam_2018_a5.lean +++ b/lean4/src/putnam_2018_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $f: \mathbb{R} \to \mathbb{R}$ be an infinitely differentiable function satisfying $f(0) = 0$, $f(1)= 1$, and $f(x) \geq 0$ for all $x \in \mathbb{R}$. Show that there exist a positive integer $n$ and a real number $x$ such that $f^{(n)}(x) < 0$. diff --git a/lean4/src/putnam_2018_a6.lean b/lean4/src/putnam_2018_a6.lean index 20891545..b6e228a4 100644 --- a/lean4/src/putnam_2018_a6.lean +++ b/lean4/src/putnam_2018_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Suppose that $A$, $B$, $C$, and $D$ are distinct points, no three of which lie on a line, in the Euclidean plane. Show that if the squares of the lengths of the line segments $AB$, $AC$, $AD$, $BC$, $BD$, and $CD$ are rational numbers, then the quotient $\frac{\text{area}(\triangle ABC)}{\text{area}(\triangle ABD)}$ is a rational number. diff --git a/lean4/src/putnam_2018_b1.lean b/lean4/src/putnam_2018_b1.lean index 37998aa5..e24f5054 100644 --- a/lean4/src/putnam_2018_b1.lean +++ b/lean4/src/putnam_2018_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2018_b1_solution : Set (Mathlib.Vector ℤ 2) := sorry -- {v : Mathlib.Vector ℤ 2 | ∃ b : ℤ, 0 ≤ b ∧ b ≤ 100 ∧ Even b ∧ v.toList = [1, b]} diff --git a/lean4/src/putnam_2018_b2.lean b/lean4/src/putnam_2018_b2.lean index cf10788f..fcdb4a70 100644 --- a/lean4/src/putnam_2018_b2.lean +++ b/lean4/src/putnam_2018_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $n$ be a positive integer, and let $f_n(z) = n + (n-1)z + (n-2)z^2 + \cdots + z^{n-1}$. Prove that $f_n$ has no roots in the closed unit disk $\{z \in \mathbb{C}: |z| \leq 1\}$. diff --git a/lean4/src/putnam_2018_b3.lean b/lean4/src/putnam_2018_b3.lean index 1b198276..c2b3ced8 100644 --- a/lean4/src/putnam_2018_b3.lean +++ b/lean4/src/putnam_2018_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2018_b3_solution : Set ℕ := sorry -- {2^2, 2^4, 2^16, 2^256} diff --git a/lean4/src/putnam_2018_b4.lean b/lean4/src/putnam_2018_b4.lean index ac973542..0209be39 100644 --- a/lean4/src/putnam_2018_b4.lean +++ b/lean4/src/putnam_2018_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Given a real number $a$, we define a sequence by $x_0 = 1$, $x_1 = x_2 = a$, and $x_{n+1} = 2x_n x_{n-1} - x_{n-2}$ for $n \geq 2$. Prove that if $x_n = 0$ for some $n$, then the sequence is periodic. diff --git a/lean4/src/putnam_2018_b5.lean b/lean4/src/putnam_2018_b5.lean index 9fba4279..bfe625c4 100644 --- a/lean4/src/putnam_2018_b5.lean +++ b/lean4/src/putnam_2018_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Function diff --git a/lean4/src/putnam_2018_b6.lean b/lean4/src/putnam_2018_b6.lean index 683c5b9d..c1700881 100644 --- a/lean4/src/putnam_2018_b6.lean +++ b/lean4/src/putnam_2018_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators /-- Let $S$ be the set of sequences of length $2018$ whose terms are in the set $\{1,2,3,4,5,6,10\}$ and sum to $3860$. Prove that the cardinality of $S$ is at most $2^{3860} \cdot \left(\frac{2018}{2048}\right)^{2018}$. diff --git a/lean4/src/putnam_2019_a1.lean b/lean4/src/putnam_2019_a1.lean index 669beed7..784a55ca 100644 --- a/lean4/src/putnam_2019_a1.lean +++ b/lean4/src/putnam_2019_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2019_a3.lean b/lean4/src/putnam_2019_a3.lean index 7eda1576..6b97c573 100644 --- a/lean4/src/putnam_2019_a3.lean +++ b/lean4/src/putnam_2019_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2019_a4.lean b/lean4/src/putnam_2019_a4.lean index 29af4c3e..dd41785d 100644 --- a/lean4/src/putnam_2019_a4.lean +++ b/lean4/src/putnam_2019_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open MeasureTheory Metric Topology Filter diff --git a/lean4/src/putnam_2019_a5.lean b/lean4/src/putnam_2019_a5.lean index 687f3267..7513289a 100644 --- a/lean4/src/putnam_2019_a5.lean +++ b/lean4/src/putnam_2019_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2019_a6.lean b/lean4/src/putnam_2019_a6.lean index 02d3a5ef..cad869ad 100644 --- a/lean4/src/putnam_2019_a6.lean +++ b/lean4/src/putnam_2019_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2019_b1.lean b/lean4/src/putnam_2019_b1.lean index 883139ae..178a6ac7 100644 --- a/lean4/src/putnam_2019_b1.lean +++ b/lean4/src/putnam_2019_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter diff --git a/lean4/src/putnam_2019_b2.lean b/lean4/src/putnam_2019_b2.lean index 4d63712c..e5bf975d 100644 --- a/lean4/src/putnam_2019_b2.lean +++ b/lean4/src/putnam_2019_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set diff --git a/lean4/src/putnam_2019_b3.lean b/lean4/src/putnam_2019_b3.lean index 4192d6ae..cc848f23 100644 --- a/lean4/src/putnam_2019_b3.lean +++ b/lean4/src/putnam_2019_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Matrix diff --git a/lean4/src/putnam_2019_b4.lean b/lean4/src/putnam_2019_b4.lean index 25243fe6..ebf76456 100644 --- a/lean4/src/putnam_2019_b4.lean +++ b/lean4/src/putnam_2019_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Matrix diff --git a/lean4/src/putnam_2019_b5.lean b/lean4/src/putnam_2019_b5.lean index fe24f2dc..3f22c963 100644 --- a/lean4/src/putnam_2019_b5.lean +++ b/lean4/src/putnam_2019_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Matrix diff --git a/lean4/src/putnam_2019_b6.lean b/lean4/src/putnam_2019_b6.lean index b453899d..a68377a6 100644 --- a/lean4/src/putnam_2019_b6.lean +++ b/lean4/src/putnam_2019_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Topology Filter Set Matrix diff --git a/lean4/src/putnam_2020_a1.lean b/lean4/src/putnam_2020_a1.lean index c99bdc8a..05d8eced 100644 --- a/lean4/src/putnam_2020_a1.lean +++ b/lean4/src/putnam_2020_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2020_a1_solution : ℕ := sorry -- 508536 diff --git a/lean4/src/putnam_2020_a2.lean b/lean4/src/putnam_2020_a2.lean index 13f0cf0a..3ac5855f 100644 --- a/lean4/src/putnam_2020_a2.lean +++ b/lean4/src/putnam_2020_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators abbrev putnam_2020_a2_solution : ℕ → ℕ := sorry -- fun k ↦ 4 ^ k diff --git a/lean4/src/putnam_2020_a3.lean b/lean4/src/putnam_2020_a3.lean index c14b2399..4f1dea64 100644 --- a/lean4/src/putnam_2020_a3.lean +++ b/lean4/src/putnam_2020_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2020_a5.lean b/lean4/src/putnam_2020_a5.lean index 18c05bfa..7fcef864 100644 --- a/lean4/src/putnam_2020_a5.lean +++ b/lean4/src/putnam_2020_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2020_a6.lean b/lean4/src/putnam_2020_a6.lean index 6200b1c3..3faa3793 100644 --- a/lean4/src/putnam_2020_a6.lean +++ b/lean4/src/putnam_2020_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2020_b1.lean b/lean4/src/putnam_2020_b1.lean index 98ed0164..46977c1a 100644 --- a/lean4/src/putnam_2020_b1.lean +++ b/lean4/src/putnam_2020_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2020_b4.lean b/lean4/src/putnam_2020_b4.lean index 54bf70ad..b196ce6d 100644 --- a/lean4/src/putnam_2020_b4.lean +++ b/lean4/src/putnam_2020_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2020_b5.lean b/lean4/src/putnam_2020_b5.lean index 3c8123b4..53b89a10 100644 --- a/lean4/src/putnam_2020_b5.lean +++ b/lean4/src/putnam_2020_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2020_b6.lean b/lean4/src/putnam_2020_b6.lean index 8f079169..2cf8d07c 100644 --- a/lean4/src/putnam_2020_b6.lean +++ b/lean4/src/putnam_2020_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Set diff --git a/lean4/src/putnam_2021_a1.lean b/lean4/src/putnam_2021_a1.lean index 9f90d042..5878df2a 100644 --- a/lean4/src/putnam_2021_a1.lean +++ b/lean4/src/putnam_2021_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2021_a2.lean b/lean4/src/putnam_2021_a2.lean index 87bf3faa..9a6d394f 100644 --- a/lean4/src/putnam_2021_a2.lean +++ b/lean4/src/putnam_2021_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2021_a3.lean b/lean4/src/putnam_2021_a3.lean index 66cbed28..f7edc72a 100644 --- a/lean4/src/putnam_2021_a3.lean +++ b/lean4/src/putnam_2021_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2021_a4.lean b/lean4/src/putnam_2021_a4.lean index 322f4832..39b49c0a 100644 --- a/lean4/src/putnam_2021_a4.lean +++ b/lean4/src/putnam_2021_a4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_2021_a5.lean b/lean4/src/putnam_2021_a5.lean index 1cf6fe80..ce8db942 100644 --- a/lean4/src/putnam_2021_a5.lean +++ b/lean4/src/putnam_2021_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2021_a6.lean b/lean4/src/putnam_2021_a6.lean index 7e3a27c0..3163a59b 100644 --- a/lean4/src/putnam_2021_a6.lean +++ b/lean4/src/putnam_2021_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2021_b2.lean b/lean4/src/putnam_2021_b2.lean index 520a067b..c191fbc7 100644 --- a/lean4/src/putnam_2021_b2.lean +++ b/lean4/src/putnam_2021_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2021_b3.lean b/lean4/src/putnam_2021_b3.lean index 345e2e51..4d64f85e 100644 --- a/lean4/src/putnam_2021_b3.lean +++ b/lean4/src/putnam_2021_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology Metric diff --git a/lean4/src/putnam_2021_b4.lean b/lean4/src/putnam_2021_b4.lean index 7d2730f0..f3f4e843 100644 --- a/lean4/src/putnam_2021_b4.lean +++ b/lean4/src/putnam_2021_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2021_b5.lean b/lean4/src/putnam_2021_b5.lean index 818e0508..26fcd540 100644 --- a/lean4/src/putnam_2021_b5.lean +++ b/lean4/src/putnam_2021_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Filter Topology diff --git a/lean4/src/putnam_2022_a1.lean b/lean4/src/putnam_2022_a1.lean index cbfc5c97..89e1d356 100644 --- a/lean4/src/putnam_2022_a1.lean +++ b/lean4/src/putnam_2022_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_a2.lean b/lean4/src/putnam_2022_a2.lean index 40ee6613..901320b7 100644 --- a/lean4/src/putnam_2022_a2.lean +++ b/lean4/src/putnam_2022_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_a3.lean b/lean4/src/putnam_2022_a3.lean index c8f42112..3755c3a6 100644 --- a/lean4/src/putnam_2022_a3.lean +++ b/lean4/src/putnam_2022_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_a6.lean b/lean4/src/putnam_2022_a6.lean index 7304b010..c3a522c6 100644 --- a/lean4/src/putnam_2022_a6.lean +++ b/lean4/src/putnam_2022_a6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_b1.lean b/lean4/src/putnam_2022_b1.lean index a100e653..86ee4f4d 100644 --- a/lean4/src/putnam_2022_b1.lean +++ b/lean4/src/putnam_2022_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_b2.lean b/lean4/src/putnam_2022_b2.lean index ce5e68c8..dd108fd5 100644 --- a/lean4/src/putnam_2022_b2.lean +++ b/lean4/src/putnam_2022_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_b3.lean b/lean4/src/putnam_2022_b3.lean index f173fd01..6932f61e 100644 --- a/lean4/src/putnam_2022_b3.lean +++ b/lean4/src/putnam_2022_b3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_b4.lean b/lean4/src/putnam_2022_b4.lean index 3915954f..fd53d102 100644 --- a/lean4/src/putnam_2022_b4.lean +++ b/lean4/src/putnam_2022_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_b5.lean b/lean4/src/putnam_2022_b5.lean index 392f2b52..880379ba 100644 --- a/lean4/src/putnam_2022_b5.lean +++ b/lean4/src/putnam_2022_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2022_b6.lean b/lean4/src/putnam_2022_b6.lean index a7848d4a..0c142355 100644 --- a/lean4/src/putnam_2022_b6.lean +++ b/lean4/src/putnam_2022_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Polynomial diff --git a/lean4/src/putnam_2023_a1.lean b/lean4/src/putnam_2023_a1.lean index 06777ee8..724bceb8 100644 --- a/lean4/src/putnam_2023_a1.lean +++ b/lean4/src/putnam_2023_a1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2023_a2.lean b/lean4/src/putnam_2023_a2.lean index eb0272d6..107e8a81 100644 --- a/lean4/src/putnam_2023_a2.lean +++ b/lean4/src/putnam_2023_a2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2023_a3.lean b/lean4/src/putnam_2023_a3.lean index 8b52da28..acbfc3e4 100644 --- a/lean4/src/putnam_2023_a3.lean +++ b/lean4/src/putnam_2023_a3.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2023_a5.lean b/lean4/src/putnam_2023_a5.lean index d1fa298e..3fce458f 100644 --- a/lean4/src/putnam_2023_a5.lean +++ b/lean4/src/putnam_2023_a5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2023_b1.lean b/lean4/src/putnam_2023_b1.lean index 949d4e47..f2dc2cb7 100644 --- a/lean4/src/putnam_2023_b1.lean +++ b/lean4/src/putnam_2023_b1.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2023_b2.lean b/lean4/src/putnam_2023_b2.lean index f3cbff51..7919457e 100644 --- a/lean4/src/putnam_2023_b2.lean +++ b/lean4/src/putnam_2023_b2.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat diff --git a/lean4/src/putnam_2023_b4.lean b/lean4/src/putnam_2023_b4.lean index 15a5d3b4..5ac2a1a8 100644 --- a/lean4/src/putnam_2023_b4.lean +++ b/lean4/src/putnam_2023_b4.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2023_b5.lean b/lean4/src/putnam_2023_b5.lean index b485ea42..49b51980 100644 --- a/lean4/src/putnam_2023_b5.lean +++ b/lean4/src/putnam_2023_b5.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter diff --git a/lean4/src/putnam_2023_b6.lean b/lean4/src/putnam_2023_b6.lean index 951078ac..106d633d 100644 --- a/lean4/src/putnam_2023_b6.lean +++ b/lean4/src/putnam_2023_b6.lean @@ -1,5 +1,4 @@ import Mathlib -open BigOperators open Nat Topology Filter