From c6661ff5bc79ce963b623b5dc4ca7b547edd851e Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Mar 2026 16:50:52 +0100 Subject: [PATCH 1/4] =?UTF-8?q?tfae=5Fhave=201=20=E2=86=92=206?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index ebae6b3..e28044a 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -4,6 +4,7 @@ import Mathlib.Data.Nat.PrimeFin import Mathlib.NumberTheory.PrimeCounting import Mathlib.SetTheory.Cardinal.Basic import Mathlib.Tactic.TFAE +import Mathlib.NumberTheory.PrimeCounting /- ## Euclid's theorem: there are infinitely many primes @@ -187,7 +188,13 @@ theorem infinitude_of_primes_tfae : [ tfae_have 1 → 2 := by sorry -- Onat - tfae_have 1 → 6 := by sorry -- Bohdan + tfae_have 1 → 6 := by + intro h + use Nat.nth Nat.Prime + use Nat.nth_injective h + intro k + exact Nat.prime_nth_prime k + -- Bohdan tfae_have 3 → 2 := by sorry -- Leonie @@ -222,4 +229,3 @@ theorem infinitude_of_primes_tfae : [ tfae_have 9 → 2 := by sorry tfae_finish - From e0c455341a268ecc1b780a613b6f052a12df65f7 Mon Sep 17 00:00:00 2001 From: Your Name Date: Thu, 12 Mar 2026 09:44:41 +0100 Subject: [PATCH 2/4] =?UTF-8?q?tfae=5Fhave=201=20=E2=86=94=207?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index e28044a..3cffc6d 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -214,13 +214,13 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 5 := by sorry -- Daniel - tfae_have 7 → 1 := by sorry -- Bohdan / Kimia + tfae_have 7 → 1 := fun _ => Nat.infinite_setOf_prime -- Bohdan / Kimia - tfae_have 1 → 7 := by sorry -- Bohdan / Kimia + tfae_have 1 → 7 := Nat.nth_strictMono -- Bohdan / Kimia tfae_have 7 → 3 := by sorry -- Kimia - tfae_have 1 → 8 := by sorry + tfae_have 1 → 8 := by sorry tfae_have 8 → 5 := by sorry From bfa4bfa0b7b9d3e75e548e7c59af388f71eedd45 Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:10:12 +0100 Subject: [PATCH 3/4] cleanup: remove duplicate import and whitespace noise, keep only proofs --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index 3cffc6d..f7b95b5 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -4,7 +4,6 @@ import Mathlib.Data.Nat.PrimeFin import Mathlib.NumberTheory.PrimeCounting import Mathlib.SetTheory.Cardinal.Basic import Mathlib.Tactic.TFAE -import Mathlib.NumberTheory.PrimeCounting /- ## Euclid's theorem: there are infinitely many primes @@ -188,13 +187,12 @@ theorem infinitude_of_primes_tfae : [ tfae_have 1 → 2 := by sorry -- Onat - tfae_have 1 → 6 := by + tfae_have 1 → 6 := by -- Bohdan intro h use Nat.nth Nat.Prime use Nat.nth_injective h intro k exact Nat.prime_nth_prime k - -- Bohdan tfae_have 3 → 2 := by sorry -- Leonie @@ -214,13 +212,13 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 5 := by sorry -- Daniel - tfae_have 7 → 1 := fun _ => Nat.infinite_setOf_prime -- Bohdan / Kimia + tfae_have 7 → 1 := fun _ => Nat.infinite_setOf_prime -- Bohdan - tfae_have 1 → 7 := Nat.nth_strictMono -- Bohdan / Kimia + tfae_have 1 → 7 := Nat.nth_strictMono -- Bohdan tfae_have 7 → 3 := by sorry -- Kimia - tfae_have 1 → 8 := by sorry + tfae_have 1 → 8 := by sorry tfae_have 8 → 5 := by sorry @@ -229,3 +227,4 @@ theorem infinitude_of_primes_tfae : [ tfae_have 9 → 2 := by sorry tfae_finish + From 9491061241e6320ecdfafce79842a6d80cfde45f Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:13:21 +0100 Subject: [PATCH 4/4] keep Bohdan / Kimia attribution for now --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index f7b95b5..463bd9e 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -212,9 +212,9 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 5 := by sorry -- Daniel - tfae_have 7 → 1 := fun _ => Nat.infinite_setOf_prime -- Bohdan + tfae_have 7 → 1 := fun _ => Nat.infinite_setOf_prime -- Bohdan / Kimia - tfae_have 1 → 7 := Nat.nth_strictMono -- Bohdan + tfae_have 1 → 7 := Nat.nth_strictMono -- Bohdan / Kimia tfae_have 7 → 3 := by sorry -- Kimia