From d9a41fcf40ba3d33f06d0b71d9630dfbedb876ae Mon Sep 17 00:00:00 2001 From: riccardobrasca Date: Mon, 4 Mar 2024 12:07:27 +0100 Subject: [PATCH] bump --- FltRegular/FLT5.lean | 26 ++------------------------ lake-manifest.json | 2 +- 2 files changed, 3 insertions(+), 25 deletions(-) diff --git a/FltRegular/FLT5.lean b/FltRegular/FLT5.lean index e5438f1c..16d2c71c 100644 --- a/FltRegular/FLT5.lean +++ b/FltRegular/FLT5.lean @@ -5,31 +5,9 @@ open Nat NumberField Polynomial IsPrimitiveRoot IsCyclotomicExtension Real Compl open scoped nonZeroDivisors theorem fermatLastTheoremFive : FermatLastTheoremFor 5 := by - classical - have five_pos : 0 < 5 := by norm_num - let p := (⟨5, five_pos⟩ : ℕ+) - have hφ : φ 5 = 4 := rfl have : Fact (Nat.Prime 5) := ⟨by norm_num⟩ - have hodd : 5 ≠ 2 := by omega - have hp : Fact (Nat.Prime (↑p : ℕ)) := this - let K := CyclotomicField p ℚ - refine flt_regular ?_ hodd + refine flt_regular ?_ (by omega) rw [IsRegularPrime, IsRegularNumber] convert coprime_one_right _ - refine classNumber_eq_one_iff.2 (RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt ?_) - suffices : discr K = 125 - rw [IsCyclotomicExtension.finrank (n := 5) K (cyclotomic.irreducible_rat five_pos), this] - · suffices InfinitePlace.NrComplexPlaces K = 2 by - · rw [this, show ((5 : ℕ+) : ℕ) = 5 by rfl, hφ, show ((4! : ℕ) : ℝ) = 24 by rfl, - abs_of_pos (by norm_num)] - norm_num - suffices (2 * (3 ^ 2 / 16) * (32 / 3)) ^ 2 < (2 * ((π : ℝ) ^ 2 / 16) * (32 / 3)) ^ 2 by - · refine lt_trans ?_ this - norm_num - gcongr - exact pi_gt_three - rw [Rat.nrComplexPlaces_eq_totient_div_two (n := 5)] - rfl - · convert IsCyclotomicExtension.Rat.absdiscr_prime p K - assumption + exact classNumber_eq_one_iff.2 (Rat.five_pid (CyclotomicField _ ℚ)) diff --git a/lake-manifest.json b/lake-manifest.json index 5920158e..b13bff0f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "86b7828a1e4debe4984e5051220a6026c8d4c6a1", + "rev": "1095e9af4d1f75960ab5485a6c5b3a851f48b5f4", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,