fixed extra 1997 thing

trishullab · Aug 1, 2024 · d7a22bb · d7a22bb
1 parent 4c2f0d6
commit d7a22bb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean4/src/putnam_1997_b5.lean b/lean4/src/putnam_1997_b5.lean
@@ -5,7 +5,7 @@ open Filter Topology Bornology Set Polynomial
 
 def tetration : ℕ → ℕ → ℕ
   | _, 0 => 1
-  | m, (n + 1) => m^(tetration m n)
+  | b, (m + 1) => b^(tetration b m)
 theorem putnam_1997_b5
 (n : ℕ)
 (hn : n ≥ 2)