From 506b30370d9a01b74e483288567ed76e62b3fd15 Mon Sep 17 00:00:00 2001 From: Christoph Spiegel Date: Thu, 12 Mar 2026 11:26:13 +0100 Subject: [PATCH] =?UTF-8?q?prove=203=20=E2=86=92=204?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean index 97091c5..9555c8a 100644 --- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean +++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean @@ -196,7 +196,9 @@ theorem infinitude_of_primes_tfae : [ tfae_have 3 → 2 := by sorry -- Leonie - tfae_have 3 → 4 := by sorry -- Alexandra + tfae_have 3 → 4 := by -- Alexandra + intro a b c + exact a b tfae_have 5 → 4 := by sorry -- Sammy