From 31b2103b6ac61d50e50c2613c42231ebaef56dd9 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 2 Jul 2024 21:44:43 +0200 Subject: [PATCH] clean more stuff --- FltRegular/FltThree/Edwards.lean | 20 ---------- FltRegular/FltThree/OddPrimeOrFour.lean | 14 ------- FltRegular/FltThree/Spts.lean | 9 ----- FltRegular/NumberTheory/CyclotomicRing.lean | 6 --- FltRegular/NumberTheory/IdealNorm.lean | 44 ++++++++++----------- FltRegular/NumberTheory/RegularPrimes.lean | 9 ----- 6 files changed, 22 insertions(+), 80 deletions(-) diff --git a/FltRegular/FltThree/Edwards.lean b/FltRegular/FltThree/Edwards.lean index 73804502..8c9f820b 100644 --- a/FltRegular/FltThree/Edwards.lean +++ b/FltRegular/FltThree/Edwards.lean @@ -380,26 +380,6 @@ theorem factorization'.associated'_of_norm_associated {a b c : ℤ√(-3)} (h : · exact factorization'.coprime_of_mem h hcmem · exact ((factorization'_prop h).2 b hbmem).2.2 -theorem factors_unique {f g : Multiset (ℤ√(-3))} (hf : ∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x).natAbs) - (hf' : ∀ x ∈ f, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x)) - (hg : ∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x).natAbs) - (hg' : ∀ x ∈ g, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x)) (h : Associated f.prod g.prod) : - Multiset.Rel Associated' f g := - by - have p : - ∀ (x : ℤ√(-3)) (_ : x ∈ f) (y : ℤ√(-3)) (_ : y ∈ g), - (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y := - by - intro x hx y hy hxy - rw [Function.comp_apply, Function.comp_apply, ← Int.associated_iff_natAbs] at hxy - apply associated'_of_associated_norm hxy - · exact hf' x hx - · exact hg' y hy - · exact hf x hx - refine' Multiset.Rel.mono _ p - rw [← Multiset.rel_map, factors_unique_prod hf hg <| Zsqrtd.associated_norm_of_associated h, - Multiset.rel_eq] - theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : Even (evenFactorExp a.norm.natAbs) := by diff --git a/FltRegular/FltThree/OddPrimeOrFour.lean b/FltRegular/FltThree/OddPrimeOrFour.lean index 0c138f64..7c0bb575 100644 --- a/FltRegular/FltThree/OddPrimeOrFour.lean +++ b/FltRegular/FltThree/OddPrimeOrFour.lean @@ -129,13 +129,6 @@ theorem oddFactors.pow (z : ℕ) (n : ℕ) : oddFactors (z ^ n) = n • oddFacto noncomputable def evenFactorExp (x : ℕ) := Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) -theorem evenFactorExp.def (x : ℕ) : - evenFactorExp x = Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) := - rfl - -theorem evenFactorExp.zero : evenFactorExp 0 = 0 := by - simp [evenFactorExp] - theorem evenFactorExp.pow (z : ℕ) (n : ℕ) : evenFactorExp (z ^ n) = n * evenFactorExp z := by simp only [evenFactorExp] @@ -170,13 +163,6 @@ theorem even_and_odd_factors' (x : ℕ) : convert even_and_odd_factors'' x simp [evenFactorExp, ← Multiset.filter_eq] -theorem even_and_oddFactors (x : ℕ) (hx : x ≠ 0) : - Associated x (2 ^ evenFactorExp x * (oddFactors x).prod) := - by - convert(UniqueFactorizationMonoid.normalizedFactors_prod hx).symm - simp [evenFactorExp] - rw [Multiset.pow_count, ← Multiset.prod_add, ← even_and_odd_factors'' x] - theorem factors_2_even {z : ℕ} (hz : z ≠ 0) : evenFactorExp (4 * z) = 2 + evenFactorExp z := by have h₀ : (4 : ℕ) ≠ 0 := four_ne_zero diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean index 96552d2a..499dc7b9 100644 --- a/FltRegular/FltThree/Spts.lean +++ b/FltRegular/FltThree/Spts.lean @@ -406,12 +406,3 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs _ = 1 := by rw [hfour] norm_num - - -theorem Spts.four_of_coprime {p : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hfour : p.norm = 4) : - abs p.re = 1 ∧ abs p.im = 1 := by - apply Spts.four hfour - rintro him - rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime - rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour - norm_num at hfour diff --git a/FltRegular/NumberTheory/CyclotomicRing.lean b/FltRegular/NumberTheory/CyclotomicRing.lean index 9a95c0df..7293fe50 100644 --- a/FltRegular/NumberTheory/CyclotomicRing.lean +++ b/FltRegular/NumberTheory/CyclotomicRing.lean @@ -124,11 +124,5 @@ lemma charZero {p} (hp : p ≠ 0) : CharZero (CyclotomicIntegers p) := instance : CharZero (CyclotomicIntegers p) := charZero hpri.out.ne_zero -open BigOperators - -lemma sum_zeta_pow : ∑ i in Finset.range p, zeta p ^ (i : ℕ) = 0 := by - rw [← AdjoinRoot.aeval_root (Polynomial.cyclotomic p ℤ), ← zeta] - simp [Polynomial.cyclotomic_prime ℤ p] - end CyclotomicIntegers end diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean index a610fe3a..bb0a3d9f 100644 --- a/FltRegular/NumberTheory/IdealNorm.lean +++ b/FltRegular/NumberTheory/IdealNorm.lean @@ -97,19 +97,19 @@ theorem spanIntNorm_singleton {r : S} : exact map_dvd _ (mem_span_singleton.mp hx'))) ((span_singleton_le_iff_mem _).mpr (intNorm_mem_spanIntNorm _ _ (mem_span_singleton_self _))) -@[simp] -theorem spanIntNorm_top : spanIntNorm R (⊤ : Ideal S) = ⊤ := by - rw [← Ideal.span_singleton_one, spanIntNorm_singleton] - simp +-- @[simp] +-- theorem spanIntNorm_top : spanIntNorm R (⊤ : Ideal S) = ⊤ := by +-- rw [← Ideal.span_singleton_one, spanIntNorm_singleton] +-- simp theorem map_spanIntNorm (I : Ideal S) {T : Type*} [CommRing T] (f : R →+* T) : map f (spanIntNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) := by rw [spanIntNorm, map_span, Set.image_image] rfl -@[mono] -theorem spanIntNorm_mono {I J : Ideal S} (h : I ≤ J) : spanIntNorm R I ≤ spanIntNorm R J := - Ideal.span_mono (Set.monotone_image h) +-- @[mono] +-- theorem spanIntNorm_mono {I J : Ideal S} (h : I ≤ J) : spanIntNorm R I ≤ spanIntNorm R J := +-- Ideal.span_mono (Set.monotone_image h) theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R⁰) {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] @@ -179,21 +179,21 @@ theorem spanIntNorm_mul_spanIntNorm_le (I J : Ideal S) : rintro _ ⟨x, hxI, y, hyJ, rfl⟩ exact Ideal.mul_mem_mul hxI hyJ -/-- This condition `eq_bot_or_top` is equivalent to being a field. -However, `Ideal.spanIntNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R` -instance to a `Field R` instance. -/ -theorem spanIntNorm_mul_of_bot_or_top [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S] - (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) : - spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J := by - refine le_antisymm ?_ (spanIntNorm_mul_spanIntNorm_le R _ _) - cases' eq_bot_or_top (spanIntNorm R I) with hI hI - · rw [hI, spanIntNorm_eq_bot_iff.mp hI, bot_mul, spanIntNorm_bot] - exact bot_le - rw [hI, Ideal.top_mul] - cases' eq_bot_or_top (spanIntNorm R J) with hJ hJ - · rw [hJ, spanIntNorm_eq_bot_iff.mp hJ, mul_bot, spanIntNorm_bot] - rw [hJ] - exact le_top +-- /-- This condition `eq_bot_or_top` is equivalent to being a field. +-- However, `Ideal.spanIntNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R` +-- instance to a `Field R` instance. -/ +-- theorem spanIntNorm_mul_of_bot_or_top [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Finite R S] +-- (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) : +-- spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J := by +-- refine le_antisymm ?_ (spanIntNorm_mul_spanIntNorm_le R _ _) +-- cases' eq_bot_or_top (spanIntNorm R I) with hI hI +-- · rw [hI, spanIntNorm_eq_bot_iff.mp hI, bot_mul, spanIntNorm_bot] +-- exact bot_le +-- rw [hI, Ideal.top_mul] +-- cases' eq_bot_or_top (spanIntNorm R J) with hJ hJ +-- · rw [hJ, spanIntNorm_eq_bot_iff.mp hJ, mul_bot, spanIntNorm_bot] +-- rw [hJ] +-- exact le_top variable [IsDomain R] [IsDomain S] [IsDedekindDomain R] [IsDedekindDomain S] diff --git a/FltRegular/NumberTheory/RegularPrimes.lean b/FltRegular/NumberTheory/RegularPrimes.lean index 5d787c40..a2da9731 100644 --- a/FltRegular/NumberTheory/RegularPrimes.lean +++ b/FltRegular/NumberTheory/RegularPrimes.lean @@ -56,15 +56,6 @@ def IsRegularNumber [hn : Fact (0 < n)] : Prop := def IsRegularPrime : Prop := IsRegularNumber p -/-- A prime number is Bernoulli regular if it does not divide the numerator of any of -the first `p - 3` (non-zero) Bernoulli numbers-/ -def IsBernoulliRegular : Prop := - ∀ i ∈ Finset.range ((p - 3) / 2), ((bernoulli 2 * i).num : ZMod p) ≠ 0 - -/-- A prime is super regular if its regular and Bernoulli regular.-/ -def IsSuperRegular : Prop := - IsRegularNumber p ∧ IsBernoulliRegular p - section TwoRegular variable (A K : Type _) [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K]