Merge pull request #256 from mo271/putnam_2022_a6

fix putnam_2022_a6
trishullab · Jan 11, 2025 · 02a8703 · 02a8703
2 parents 83d8626 + 107eb69
commit 02a8703
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean4/src/putnam_2022_a6.lean b/lean4/src/putnam_2022_a6.lean
@@ -13,6 +13,6 @@ theorem putnam_2022_a6
     IsGreatest
       {m : ℕ | ∃ x : ℕ → ℝ,
         StrictMono x ∧ -1 < x 1 ∧ x (2 * n) < 1 ∧
-        ∀ k ∈ Icc 1 m, ∑ i in Finset.Icc 1 n, ((x (2 * i - 1) : ℝ) ^ (2 * k - 1) - (x (2 * i)) ^ (2 * k - 1)) = 1}
+        ∀ k ∈ Icc 1 m, ∑ i in Icc 1 n, ((x (2 * i) : ℝ) ^ (2 * k - 1) - (x (2 * i - 1)) ^ (2 * k - 1)) = 1}
     (putnam_2022_a6_solution n) :=
   sorry