From 578c3cfe2d72057d4afe0a6c0066bacc485bcf26 Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Fri, 5 Sep 2025 14:55:49 +0200 Subject: [PATCH 1/3] typo --- .../S02_Induction_and_Recursion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean index 5ccc41b..332d4ef 100644 --- a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean +++ b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean @@ -32,7 +32,7 @@ The command specifies that ``Nat`` is the datatype generated freely and inductively by the two constructors ``zero : Nat`` and ``succ : Nat → Nat``. Of course, the library introduces notation ``ℕ`` and ``0`` for -``nat`` and ``zero`` respectively. (Numerals are translated to binary +``Nat`` and ``zero`` respectively. (Numerals are translated to binary representations, but we don't have to worry about the details of that now.) What "freely" means for the working mathematician is that the type From 03cbbffff3dfc9119f862d0116dfcf2a11675b23 Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Fri, 5 Sep 2025 14:56:57 +0200 Subject: [PATCH 2/3] spaces --- MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean b/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean index f83cd70..b606e49 100644 --- a/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean +++ b/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean @@ -246,10 +246,10 @@ theorem ne_one_iff_exists_prime_dvd : ∀ {n}, n ≠ 1 ↔ ∃ p : ℕ, p.Prime | 0 => by simpa using Exists.intro 2 Nat.prime_two | 1 => by simp [Nat.not_prime_one] | n + 2 => by - have hn : n+2 ≠ 1 := by omega + have hn : n + 2 ≠ 1 := by omega simp only [Ne, not_false_iff, true_iff, hn] by_cases h : Nat.Prime (n + 2) - · use n+2, h + · use n + 2, h · have : 2 ≤ n + 2 := by omega rw [Nat.not_prime_iff_exists_dvd_lt this] at h rcases h with ⟨m, mdvdn, mge2, -⟩ From 1879c0e27d75ddd4310afeb0a82efd65aba3609e Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Fri, 5 Sep 2025 15:53:18 +0200 Subject: [PATCH 3/3] solution shows up in examples --- .../S04_More_Induction.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean b/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean index b606e49..cf792a0 100644 --- a/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean +++ b/MIL/C05_Elementary_Number_Theory/S04_More_Induction.lean @@ -218,16 +218,14 @@ theorem fib_add' : ∀ m n, fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib /- TEXT: As an exercise, use ``fib_add`` to prove the following. -EXAMPLES: -/ --- QUOTE: -example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by sorry --- QUOTE. -/- SOLUTIONS: -example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by - rw [two_mul, fib_add, pow_two, pow_two] BOTH: -/ +-- QUOTE: example (n : ℕ): (fib n) ^ 2 + (fib (n + 1)) ^ 2 = fib (2 * n + 1) := by +/- EXAMPLES: + sorry +SOLUTIONS: -/ rw [two_mul, fib_add, pow_two, pow_two] +-- QUOTE. /- TEXT: Lean's mechanisms for defining recursive functions are flexible enough to allow arbitrary