fix the problems

trishullab · Aug 21, 2024 · 1c469e6 · 1c469e6
1 parent 4194fb1
commit 1c469e6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/lean4/src/putnam_2007_a3.lean b/lean4/src/putnam_2007_a3.lean
@@ -2,6 +2,7 @@ import Mathlib
 open BigOperators
 
 open Set
+open scoped Nat
 
 abbrev putnam_2007_a3_solution : ℕ → ℚ := sorry
 -- fun k ↦ (k)! * (k + 1)! / ((3 * k + 1) * (2 * k)!)

diff --git a/lean4/src/putnam_2016_a2.lean b/lean4/src/putnam_2016_a2.lean
@@ -4,7 +4,7 @@ open BigOperators
 open Polynomial Filter Topology Real Set Nat
 
 noncomputable abbrev putnam_2016_a2_solution : ℝ := sorry
--- (3 + sqrt 5) / 2
+-- (3 + √ 5) / 2
 theorem putnam_2016_a2
 (p : ℕ → ℕ → Prop)
 (hp : p = fun n ↦ fun m ↦ Nat.choose m (n - 1) > Nat.choose (m - 1) n)