From cdfa2f1acd89535873c70bf1b7de4361eaeb67fe Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 2 May 2024 18:00:18 +0200 Subject: [PATCH 1/6] wip --- FltRegular/CaseI/AuxLemmas.lean | 14 +++--- FltRegular/FltThree/Edwards.lean | 4 +- FltRegular/FltThree/FltThree.lean | 11 ++-- FltRegular/FltThree/Spts.lean | 8 +-- FltRegular/MayAssume/Lemmas.lean | 2 +- .../NumberTheory/Cyclotomic/CyclRat.lean | 13 ++--- .../NumberTheory/Cyclotomic/Factoring.lean | 2 +- .../Cyclotomic/GaloisActionOnCyclo.lean | 2 +- .../NumberTheory/Cyclotomic/MoreLemmas.lean | 2 +- .../NumberTheory/Cyclotomic/UnitLemmas.lean | 5 +- FltRegular/NumberTheory/GaloisPrime.lean | 8 +-- FltRegular/NumberTheory/QuotientTrace.lean | 6 +-- FltRegular/NumberTheory/Unramified.lean | 1 + .../ReadyForMathlib/Homogenization.lean | 16 +++--- FltRegular/ReadyForMathlib/PowerBasis.lean | 3 +- lake-manifest.json | 50 +++---------------- lakefile.lean | 4 +- lean-toolchain | 2 +- 18 files changed, 59 insertions(+), 94 deletions(-) diff --git a/FltRegular/CaseI/AuxLemmas.lean b/FltRegular/CaseI/AuxLemmas.lean index 249f0170..cd705c7a 100644 --- a/FltRegular/CaseI/AuxLemmas.lean +++ b/FltRegular/CaseI/AuxLemmas.lean @@ -46,8 +46,8 @@ theorem auxf0k₁ (hp5 : 5 ≤ p) (b : ℤ) : ∃ i : Fin P, f0k₁ b p (i : ℕ intro h simp only [Fin.ext_iff, Fin.val_mk] at h replace h := h.symm - rw [Nat.pred_eq_succ_iff] at h - linarith + rw [Nat.pred_eq_sub_one] at h + omega simp only [f0k₁, OfNat.ofNat_ne_one, ite_false, ite_eq_right_iff, neg_eq_zero] intro h2 exfalso @@ -65,9 +65,9 @@ theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₁ b p j • ζ ^ j := by convert hdiv using 1 have h : 1 ≠ p.pred := fun h => by linarith [pred_eq_succ_iff.1 h.symm] - simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right h, + simp_rw [f0k₁, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h, Finset.range_filter_eq] - simp [hpri.one_lt, pred_lt hpri.ne_zero, sub_eq_add_neg] + simp [hpri.one_lt, Nat.sub_lt hpri.pos, sub_eq_add_neg] rw [sum_range] at key refine' caseI (Dvd.dvd.mul_right (Dvd.dvd.mul_left _ _) _) replace hpri : (P : ℕ).Prime := hpri @@ -112,10 +112,10 @@ theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ ← sub_mul, add_sub_right_comm, show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₂ a b j • ζ ^ j := by convert hdiv using 1 - simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right zero_ne_one, + simp_rw [f0k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right zero_ne_one, Finset.range_filter_eq] simp only [hpri.pos, hpri.one_lt, if_true, zsmul_eq_mul, Int.cast_sub, sum_singleton, - _root_.pow_zero, mul_one, pow_one, Ne.def, zero_smul, sum_const_zero, add_zero, Fin.val_mk] + _root_.pow_zero, mul_one, pow_one, Ne, zero_smul, sum_const_zero, add_zero, Fin.val_mk] rw [sum_range] at key refine' hab _ symm @@ -194,7 +194,7 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by rwa [this] - simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right + simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right (show 0 ≠ 2 by norm_num), Finset.range_filter_eq] simp only [hpri.pos, ite_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, mul_one, two_lt hp5, neg_smul, sum_neg_distrib, ne_eq, mem_range, not_and, not_not, zero_smul, sum_const_zero, add_zero] diff --git a/FltRegular/FltThree/Edwards.lean b/FltRegular/FltThree/Edwards.lean index 9938f576..948d5fd8 100644 --- a/FltRegular/FltThree/Edwards.lean +++ b/FltRegular/FltThree/Edwards.lean @@ -198,7 +198,7 @@ theorem OddPrimeOrFour.factors' {a : ℤ√(-3)} (h2 : a.norm ≠ 1) (hcoprime : obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp hd use u cases' huv with huv huv <;> [(use q'); (use star q')] <;> - simp only [IsCoprime, Zsqrtd.star_re, Zsqrtd.star_im, Ne.def, neg_eq_zero, Zsqrtd.norm_conj] <;> + simp only [IsCoprime, Zsqrtd.star_re, Zsqrtd.star_im, Ne, neg_eq_zero, Zsqrtd.norm_conj] <;> use hc, hd, hp, huv, huvcoprime <;> · rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← Zsqrt3.norm_natAbs, Nat.one_lt_cast] @@ -324,7 +324,7 @@ theorem no_conj (s : Multiset (ℤ√(-3))) {p : ℤ√(-3)} (hp : ¬IsUnit p) rw [← Int.isUnit_iff_abs_eq] apply IsCoprime.isUnit_of_dvd' hcoprime <;> apply dvd_mul_right · have : star p ≠ p := by - rw [Ne.def, Zsqrtd.ext_iff] + rw [Ne, Zsqrtd.ext_iff] rintro ⟨-, H⟩ apply him apply eq_zero_of_neg_eq diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean index 18703f26..172567de 100644 --- a/FltRegular/FltThree/FltThree.lean +++ b/FltRegular/FltThree/FltThree.lean @@ -212,7 +212,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : by intro d hdprime hdleft hdright by_contra hne3 - rw [← Ne.def] at hne3 + rw [← Ne] at hne3 apply (Nat.prime_iff_prime_int.mp hdprime).not_unit have hne2 : d ≠ 2 := by rintro rfl @@ -457,8 +457,7 @@ theorem descent_gcd1 (a b c p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) simp only [‹¬ Even (3 : ℤ)›, false_or_iff, iff_not_self, parity_simps] at huvodd · intro H rw [add_eq_zero_iff_eq_neg] at H - apply iff_not_self - simpa [‹¬ Even (3 : ℤ)›, H, parity_simps] using huvodd + simp [‹¬ Even (3 : ℤ)›, H, parity_simps] at huvodd · apply Int.gcd1_coprime12 u v <;> assumption · apply Int.gcd1_coprime13 u v <;> assumption · apply Int.gcd1_coprime23 u v <;> assumption @@ -627,12 +626,10 @@ theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime : · exact mul_ne_zero two_ne_zero hv · intro H rw [sub_eq_zero] at H - apply iff_not_self - simpa [H, parity_simps] using huvodd + simp [H, parity_simps] at huvodd · intro H rw [add_eq_zero_iff_eq_neg] at H - apply iff_not_self - simpa [H, parity_simps] using huvodd + simp [H, parity_simps] at huvodd · exact hsubcoprime · exact haddcoprime · exact haddsubcoprime diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean index 524f6927..dc674df3 100644 --- a/FltRegular/FltThree/Spts.lean +++ b/FltRegular/FltThree/Spts.lean @@ -13,9 +13,9 @@ theorem Zsqrtd.exists {d : ℤ} (a : ℤ√d) (him : a.im ≠ 0) : cases' le_or_lt a.re 0 with hre hre · use -a simp only [hre, him, Zsqrtd.norm_neg, eq_self_iff_true, Zsqrtd.neg_im, Zsqrtd.neg_re, - and_self_iff, neg_nonneg, Ne.def, not_false_iff, neg_eq_zero] + and_self_iff, neg_nonneg, Ne, not_false_iff, neg_eq_zero] · use a - simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne.def, not_false_iff] + simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne, not_false_iff] -- Edwards p49 step (2') theorem factors2 {a : ℤ√(-3)} (heven : Even a.norm) : ∃ b : ℤ√(-3), a.norm = 4 * b.norm := @@ -248,7 +248,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod have hneg1 : 1 ≤ a.norm := by rw [← Int.sub_one_lt_iff, sub_self] apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a) - rw [Ne.def, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)] + rw [Ne, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)] rintro rfl rw [Zsqrtd.zero_im, Zsqrtd.zero_re] at hcoprime exact not_isCoprime_zero_zero hcoprime @@ -261,7 +261,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod refine' ⟨⟨1, 0⟩, _⟩ norm_num [Zsqrtd.norm_def] obtain ⟨c', m, rfl, -, h1, ⟨y, hy, h3⟩⟩ := Zqrtd.factor_div' a hodd h hcoprime hfactor - have h4 : c'.norm ≠ 0 := by rwa [Ne.def, Zsqrtd.norm_eq_zero_iff (by norm_num) c'] + have h4 : c'.norm ≠ 0 := by rwa [Ne, Zsqrtd.norm_eq_zero_iff (by norm_num) c'] set g := Int.gcd c'.re c'.im with hg have hgpos : 0 < g := by rwa [hg, Zsqrtd.gcd_pos_iff] obtain ⟨C', HC', HCDcoprime⟩ := Zsqrtd.exists_coprime_of_gcd_pos hgpos diff --git a/FltRegular/MayAssume/Lemmas.lean b/FltRegular/MayAssume/Lemmas.lean index 7f103172..207afc38 100644 --- a/FltRegular/MayAssume/Lemmas.lean +++ b/FltRegular/MayAssume/Lemmas.lean @@ -88,7 +88,7 @@ theorem a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp5 : 5 ≤ p) (h · simp only [mem_insert, mem_singleton] at hx rcases hx with (H | H | H) <;> simp [H] rw [this] - simp only [gcd_insert, id.def, gcd_singleton, normalize_apply, neg_mul] + simp only [gcd_insert, id, gcd_singleton, normalize_apply, neg_mul] congr 1 rw [← coe_gcd, ← coe_gcd, Int.gcd_eq_natAbs, Int.gcd_eq_natAbs] simp only [natAbs_neg, Nat.cast_inj] diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean index 5a9d363c..5195f849 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean @@ -291,7 +291,7 @@ lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ} rw [← eq_top_iff_one] at hone have hcontra := IsPrime.ne_top hPrime rw [hone] at hcontra - simp only [Ne.def, eq_self_iff_true, not_true] at hcontra + simp only [Ne, eq_self_iff_true, not_true] at hcontra apply HC hprime3 apply HC hprime2 @@ -349,9 +349,9 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} set b := hζ'.integralPowerBasis' with hb have hdim : b.dim = (p : ℕ).pred := by rw [hζ'.power_basis_int'_dim, totient_prime hp.out, pred_eq_sub_one] - by_cases H : i = ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ + by_cases H : i = ⟨(p : ℕ) - 1, pred_lt hp.out.ne_zero⟩ · simp [H.symm, Hi] - have hi : ↑i < (p : ℕ).pred := by + have hi : ↑i < (p : ℕ) - 1 := by by_contra! habs simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt i))] at H obtain ⟨y, hy⟩ := hdiv @@ -383,7 +383,8 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} rw [hn] at hy simp only [Fin.castIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Hi, zero_sub, neg_eq_iff_eq_neg] at hy - simp [hy, dvd_neg] + erw [hy] -- pred vs - 1 + simp [dvd_neg] theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPrimitiveRoot ζ p) {f : Fin p → ℤ} (hf : ∃ i, f i = 0) {m : ℤ} (hdiv : ↑m ∣ ∑ j, f j • ζ ^ (j : ℕ)) : @@ -401,9 +402,9 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri pred_eq_sub_one] have last_dvd := dvd_last_coeff_cycl_integer hζ hf hdiv intro j - by_cases H : j = ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩ + by_cases H : j = ⟨(p : ℕ) - 1, pred_lt hp.ne_zero⟩ · simpa [H] using last_dvd - have hj : ↑j < (p : ℕ).pred := by + have hj : ↑j < (p : ℕ) - 1 := by by_contra! habs simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H obtain ⟨y, hy⟩ := hdiv diff --git a/FltRegular/NumberTheory/Cyclotomic/Factoring.lean b/FltRegular/NumberTheory/Cyclotomic/Factoring.lean index ace01a02..2b29ac51 100644 --- a/FltRegular/NumberTheory/Cyclotomic/Factoring.lean +++ b/FltRegular/NumberTheory/Cyclotomic/Factoring.lean @@ -36,7 +36,7 @@ theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul {K : Type _} [CommRing K] [IsDom -- the homogenization of the identity is also true have := congr_arg (homogenization 1) this -- simplify to get the result we want - simpa [homogenization_prod, algebraMap_eq, hpos] + simpa [homogenization_prod, Polynomial.algebraMap_eq, hpos] /-- If there is a primitive `n`th root of unity in `K` and `n` is odd, then `X ^ n + Y ^ n = ∏ (X + μ Y)`, where `μ` varies over the `n`-th roots of unity. -/ diff --git a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean index ca112da5..269b60eb 100644 --- a/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean +++ b/FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean @@ -1,6 +1,6 @@ import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits import Mathlib.NumberTheory.Cyclotomic.Gal -import Mathlib.NumberTheory.NumberField.Units +import Mathlib.NumberTheory.NumberField.Units.Basic universe u diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean index 5b0cecb4..b48862aa 100644 --- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean @@ -24,7 +24,7 @@ lemma IsPrimitiveRoot.prime_span_sub_one : Prime (Ideal.span <| singleton <| (h rw [Ideal.prime_iff_isPrime, Ideal.span_singleton_prime (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)] exact hζ.zeta_sub_one_prime' - · rw [Ne.def, Ideal.span_singleton_eq_bot] + · rw [Ne, Ideal.span_singleton_eq_bot] exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) - 1 : 𝓞 K) = p := by diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean index c12caddd..57027d33 100644 --- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean @@ -155,6 +155,7 @@ theorem aux {t} {l : 𝓞 K} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot (h : ∑ x : Fin t, f x • (⟨μ, hμ.isIntegral p.pos⟩ : 𝓞 K) ^ (x : ℕ) = l) : algebraMap (𝓞 K) (𝓞 K ⧸ I) l = ∑ x : Fin t, (f x : 𝓞 K ⧸ I) := by apply_fun algebraMap (𝓞 K) (𝓞 K ⧸ I) at h + stop simp only [map_sum, map_zsmul] at h convert h.symm using 1 congr @@ -242,7 +243,7 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K) have isPrimRoot : IsPrimitiveRoot (hζ.unit' : R) p := hζ.unit'_coe have hxl : (⟨x, hx⟩ : R) ^ l = 1 := by apply isRoot_of_unity_of_root_cyclotomic _ hhl - simp only [Nat.mem_divisors, dvd_refl, Ne.def, true_and_iff] + simp only [Nat.mem_divisors, dvd_refl, Ne, true_and_iff] apply pos_iff_ne_zero.1 (Nat.pos_of_mem_divisors hl) have hxp' : (⟨x, hx⟩ : R) ^ (2 * p : ℕ) = 1 := by cases' hlp with hlp_w hlp_h @@ -292,7 +293,7 @@ theorem IsPrimitiveRoot.isPrime_one_sub_zeta [hp : Fact (p : ℕ).Prime] : · exact hζ.zeta_sub_one_prime' apply_fun (fun x : 𝓞 K => (x : K)) push_cast - rw [Ne.def, sub_eq_zero] + rw [Ne, sub_eq_zero] rintro rfl exact hp.1.ne_one (hζ.unique IsPrimitiveRoot.one) diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean index a096c8d8..0b7be229 100644 --- a/FltRegular/NumberTheory/GaloisPrime.lean +++ b/FltRegular/NumberTheory/GaloisPrime.lean @@ -57,7 +57,7 @@ lemma coe_primesOverFinset [Ring.DimensionLEOne R] [IsDedekindDomain S] classical ext P have : p.map (algebraMap R S) ≠ ⊥ := by - rwa [Ne.def, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)] + rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)] simp only [Finset.mem_coe, Multiset.mem_toFinset, Ideal.mem_normalizedFactors_iff this, factors_eq_normalizedFactors, Ideal.map_le_iff_le_comap, primesOverFinset] exact ⟨fun H ↦ ⟨H.1, ((hp'.isMaximal hp).eq_of_le (H.1.comap _).ne_top H.2).symm⟩, @@ -327,7 +327,7 @@ lemma ramificationIdxIn_smul_primesOverFinset [IsDedekindDomain S] Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _ hP'.1 (ne_bot_of_mem_primesOver hp hP'), primesOverFinset, Multiset.toFinset_val, Multiset.count_dedup, if_pos hP, mul_one] - rwa [Ne.def, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective _ _)] + rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective _ _)] lemma prod_primesOverFinset_pow_ramificationIdxIn [IsDedekindDomain S] [IsGalois K L] (p : Ideal R) (hp : p ≠ ⊥) [p.IsMaximal] : @@ -341,7 +341,7 @@ lemma prod_primesOverFinset_pow_ramificationIdxIn [IsDedekindDomain S] [IsGalois simp only [Multiset.toFinset_val, Multiset.map_id', ← Multiset.prod_nsmul, ramificationIdxIn_smul_primesOverFinset K L, ← associated_iff_eq] apply factors_prod - rwa [Ne.def, Ideal.zero_eq_bot, Ideal.map_eq_bot_iff_of_injective hRS] + rwa [Ne, Ideal.zero_eq_bot, Ideal.map_eq_bot_iff_of_injective hRS] lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p.IsMaximal] : ∏ σ : L ≃ₐ[K] L, (↑(σ • P) : Ideal S) = (p.map (algebraMap R S)) ^ (p.inertiaDegIn S) := by @@ -364,7 +364,7 @@ lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p. Ideal.comap_bot_of_injective _ (galRestrict R K L S _).injective, Finset.prod_const, Ideal.map_bot, Ideal.inertiaDegIn_bot R S (IsIntegralClosure.isIntegral_algebra R L)] refine (zero_pow ?_).trans (zero_pow ?_).symm - · rw [Finset.card_univ, Ne.def, Fintype.card_eq_zero_iff] + · rw [Finset.card_univ, Ne, Fintype.card_eq_zero_iff] simp only [not_isEmpty_of_nonempty, not_false_eq_true] · have hR := not_imp_not.mp (Ring.ne_bot_of_isMaximal_of_not_isField ‹_›) rfl letI : Field R := hR.toField diff --git a/FltRegular/NumberTheory/QuotientTrace.lean b/FltRegular/NumberTheory/QuotientTrace.lean index 1b79ddba..578da36d 100644 --- a/FltRegular/NumberTheory/QuotientTrace.lean +++ b/FltRegular/NumberTheory/QuotientTrace.lean @@ -152,7 +152,7 @@ def equivQuotMaximalIdealOfIsLocalization : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal mul_left_comm, ← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, map_mul, hs, mul_inv_cancel, mul_one, sub_self] - rw [Ne.def, Ideal.Quotient.eq_zero_iff_mem] + rw [Ne, Ideal.Quotient.eq_zero_iff_mem] exact s.prop local notation "pS" => Ideal.map (algebraMap R S) p @@ -184,7 +184,7 @@ lemma comap_map_eq_map_of_isLocalization_algebraMapSubmonoid : refine ⟨β, β * α - 1, ?_, ?_⟩ · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, map_mul, hβ, inv_mul_cancel, sub_self] - rwa [Ne.def, Ideal.Quotient.eq_zero_iff_mem] + rwa [Ne, Ideal.Quotient.eq_zero_iff_mem] · rw [add_sub_cancel] have := Ideal.mul_mem_left _ (algebraMap _ _ β) hαx rw [← Algebra.smul_def, smul_smul, hβ, add_smul, one_smul] at this @@ -215,7 +215,7 @@ def quotMapEquivQuotMapMaximalIdealOfIsLocalization : S ⧸ pS ≃+* Sₚ ⧸ pS refine ⟨β, α * β - 1, ?_, ?_⟩ · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, map_mul, hβ, mul_inv_cancel, sub_self] - rwa [Ne.def, Ideal.Quotient.eq_zero_iff_mem] + rwa [Ne, Ideal.Quotient.eq_zero_iff_mem] · rw [add_sub_cancel] use β • x rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq, diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean index fb9a902d..9dce864e 100644 --- a/FltRegular/NumberTheory/Unramified.lean +++ b/FltRegular/NumberTheory/Unramified.lean @@ -214,6 +214,7 @@ lemma isUnramifiedAt_of_Separable_minpoly' [IsSeparable K L] simp only [← Ideal.Quotient.algebraMap_eq, ← map_map, derivative_map, map_add, map_mul, aeval_map_algebraMap, aeval_algebraMap_apply, minpoly.aeval, map_zero, mul_zero, hxP, zero_add, coe_aeval_eq_eval, eval_one] at e + stop exact zero_ne_one e · rwa [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _ (isMaximal_of_mem_primesOver hpbot hP).isPrime (ne_bot_of_mem_primesOver hpbot hP), diff --git a/FltRegular/ReadyForMathlib/Homogenization.lean b/FltRegular/ReadyForMathlib/Homogenization.lean index 4e51f573..0474015a 100644 --- a/FltRegular/ReadyForMathlib/Homogenization.lean +++ b/FltRegular/ReadyForMathlib/Homogenization.lean @@ -89,7 +89,7 @@ theorem support_mapDomain {α β M : Type _} [AddCommMonoid M] (f : α ↪ β) ( classical rw [Finsupp.mapDomain] refine' Finset.Subset.trans Finsupp.support_sum _ - simp only [Finsupp.mem_support_iff, Finset.biUnion_subset_iff_forall_subset, Ne.def] + simp only [Finsupp.mem_support_iff, Finset.biUnion_subset_iff_forall_subset, Ne] intro x hx apply Finset.Subset.trans Finsupp.support_single_subset simp [hx] @@ -343,13 +343,13 @@ theorem leadingTerms_eq_self_iff_isHomogeneous (p : MvPolynomial ι R) : · rw [IsHomogeneous, IsWeightedHomogeneous] contrapose! h rcases h with ⟨h_w, h_h₁, h_h₂⟩ - rw [leadingTerms, Ne.def, MvPolynomial.ext_iff] + rw [leadingTerms, Ne, MvPolynomial.ext_iff] push_neg use h_w classical rw [weightedDegree_one] at h_h₂ change ¬(h_w.sum fun (_x : ι) (e : ℕ) => e) = p.totalDegree at h_h₂ - simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne.def, + simp only [h_h₁.symm, coeff_homogeneousComponent, exists_prop, and_true_iff, Ne, not_false_iff, not_forall, ite_eq_left_iff] convert h_h₂ · rw [leadingTerms_apply] @@ -451,7 +451,7 @@ theorem support_sum_monomial_subset (S : Finset (ι →₀ ℕ)) (f : (ι →₀ theorem sum_monomial_ne_zero_of_exists_mem_ne_zero (S : Finset (ι →₀ ℕ)) (f : (ι →₀ ℕ) → R) (h : ∃ (s : _) (_ : s ∈ S), f s ≠ 0) : ∑ s : ι →₀ ℕ in S, monomial s (f s) ≠ 0 := by classical - simp only [← support_eq_empty, support_sum_monomial_eq, Ne.def] + simp only [← support_eq_empty, support_sum_monomial_eq, Ne] rcases h with ⟨s, h_S, h_s⟩ exact ne_empty_of_mem (mem_filter.mpr ⟨h_S, h_s⟩) @@ -606,7 +606,7 @@ theorem eq_C_of_totalDegree_zero {p : MvPolynomial ι R} (hp : p.totalDegree = 0 apply hm rw [Finsupp.sum] at hp -- TODO this and line below could be a lemma, finsupp.sum_eq_zero_iff? - simp only [not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] at hp + simp only [_root_.not_imp_self, bot_eq_zero, Finsupp.mem_support_iff, Finset.sum_eq_zero_iff] at hp ext simp [hp] @@ -845,7 +845,7 @@ theorem support_prod (P : Finset (MvPolynomial ι R)) : (P.prod id).support ⊆ induction' P using Finset.induction with p S hS hSi · simp only [prod_empty, sum_empty]; exact support_one rw [Finset.prod_insert hS, Finset.sum_insert hS] - simp only [id.def] + simp only [id] refine' Finset.Subset.trans (support_mul' _ _) _ convert Finset.add_subset_add (Finset.Subset.refl _) hSi @@ -881,7 +881,7 @@ theorem prod_contains_no (i : ι) (P : Finset (MvPolynomial ι R)) apply Nat.eq_zero_of_le_zero apply le_trans (degreeOf_mul_le _ _ _) rw [hs] - · simp only [id.def, add_zero, le_zero_iff] + · simp only [id, add_zero, le_zero_iff] exact (degreeOf_eq_zero_iff _ _).2 (hp a (mem_cons_self _ _)) · intro p hps m hmp apply hp p _ m hmp @@ -908,6 +908,6 @@ theorem homogenization_prod_id {S : Type _} [CommRing S] [IsDomain S] (i : ι) simp only [Finset.prod_insert hS] rw [homogenization_mul] rw [hSi] - rw [id.def] + rw [id] end MvPolynomial diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean index 8bae9784..2be44e54 100644 --- a/FltRegular/ReadyForMathlib/PowerBasis.lean +++ b/FltRegular/ReadyForMathlib/PowerBasis.lean @@ -7,7 +7,8 @@ open RingOfIntegers Ideal Finset Nat FiniteDimensional variable {K : Type _} [Field K] (pb : PowerBasis ℤ (𝓞 K)) -instance : Module (𝓞 K) (𝓞 K) := Semiring.toModule +instance instModuleSubtypeMemSubalgebraIntRingOfIntegers_fltRegular_bis : + Module (𝓞 K) (𝓞 K) := Semiring.toModule theorem exists_int_sModEq (x : 𝓞 K) : ∃ (n : ℤ), SModEq (span ({ pb.gen } : Set (𝓞 K))) x n := by diff --git a/lake-manifest.json b/lake-manifest.json index 37e80fc4..648a1159 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb", + "rev": "3025cb124492b423070f20cf0a70636f757d117f", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", + "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,16 +31,16 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.35", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", + "rev": "188eb34fcf1125e89d651ad462d02598219718ca", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,47 +58,11 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "e9bc16347b34a91a7498edb615179b5788bf1ed4", + "rev": "4e159e0ef38e6e7894342429440ec9b4f5011bfd", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/xubaiw/CMark.lean", - "type": "git", - "subDir": null, - "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", - "name": "CMark", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hargonix/LeanInk", - "type": "git", - "subDir": null, - "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f", - "name": "leanInk", - "manifestFile": "lake-manifest.json", - "inputRev": "doc-gen", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "rev": "a34d3c1f7b72654c08abe5741d94794db40dbb2e", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, "configFile": "lakefile.lean"}], "name": "«flt-regular»", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 758848d5..90ad3c86 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,8 +8,8 @@ package «flt-regular» { require mathlib from git "https://github.com/leanprover-community/mathlib4.git" -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "main" +--require «doc-gen4» from git +-- "https://github.com/leanprover/doc-gen4" @ "main" @[default_target] lean_lib «FltRegular» { diff --git a/lean-toolchain b/lean-toolchain index 9ad30404..d8a6d7ef 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.8.0-rc1 From c27963eb80fbe036cf9d6002f77ea78b3ddb19f8 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 2 May 2024 21:07:43 +0200 Subject: [PATCH 2/6] more --- FltRegular/CaseI/Statement.lean | 4 ++-- FltRegular/CaseII/AuxLemmas.lean | 16 ++++++++-------- FltRegular/NumberTheory/Hilbert92.lean | 6 ++---- FltRegular/NumberTheory/Hilbert94.lean | 2 +- FltRegular/NumberTheory/KummersLemma/Field.lean | 2 +- .../NumberTheory/KummersLemma/KummersLemma.lean | 2 +- 6 files changed, 15 insertions(+), 17 deletions(-) diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index 3036d9ff..ccdfaa91 100644 --- a/FltRegular/CaseI/Statement.lean +++ b/FltRegular/CaseI/Statement.lean @@ -237,11 +237,11 @@ theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p) have h1k₁ := aux1k₁ hpri.out hp5 hζ hab hcong hdiv have h1k₂ := aux1k₂ hpri.out hp5 hζ caseI hcong hdiv have hk₁k₂ : (k₁ : ℕ) ≠ (k₂ : ℕ) := auxk₁k₂ hpri.out hcong - simp_rw [f, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right h01, and_assoc, + simp_rw [f, ite_smul, sum_ite, filter_filter, ← Ne.eq_def, ne_and_eq_iff_right h01, and_assoc, ne_and_eq_iff_right h1k₁, ne_and_eq_iff_right h0k₁, ne_and_eq_iff_right hk₁k₂, ne_and_eq_iff_right h1k₂, ne_and_eq_iff_right h0k₂, Finset.range_filter_eq] simp only [hpri.out.pos, hpri.out.one_lt, if_true, zsmul_eq_mul, sum_singleton, _root_.pow_zero, - mul_one, pow_one, Fin.is_lt, neg_smul, sum_neg_distrib, Ne.def, zero_smul, sum_const_zero, + mul_one, pow_one, Fin.is_lt, neg_smul, sum_neg_distrib, Ne, zero_smul, sum_const_zero, add_zero] ring rw [sum_range] at key diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean index 20e65b52..de57340f 100644 --- a/FltRegular/CaseII/AuxLemmas.lean +++ b/FltRegular/CaseII/AuxLemmas.lean @@ -44,7 +44,7 @@ lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CancelCommMonoidWithZero {x y : M} : multiplicity.Finite x y ↔ ¬IsUnit x ∧ y ≠ 0 := by constructor - · rw [← not_imp_not, Ne.def, ← not_or, not_not] + · rw [← not_imp_not, Ne, ← not_or, not_not] rintro (hx|hy) · exact fun ⟨n, hn⟩ ↦ hn (hx.pow _).dvd · simp [hy] @@ -135,7 +135,7 @@ theorem isPrincipal_of_isPrincipal_pow_of_Coprime' by_cases Izero : I = 0 · rw [Izero, FractionalIdeal.coe_zero] exact bot_isPrincipal - rw [← Ne.def, ← isUnit_iff_ne_zero] at Izero + rw [← Ne, ← isUnit_iff_ne_zero] at Izero show Submodule.IsPrincipal (Izero.unit' : FractionalIdeal A⁰ K) rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff] refine ⟨?_, orderOf_dvd_card⟩ @@ -153,9 +153,9 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD ∃ a b : R, ¬(x ∣ a) ∧ ¬(x ∣ b) ∧ spanSingleton R⁰ (algebraMap R K a / algebraMap R K b) = I / J := by by_contra H1 have hI' : (I : FractionalIdeal R⁰ K) ≠ 0 := - by rw [← coeIdeal_bot, Ne.def, coeIdeal_inj]; rintro rfl; exact hI (dvd_zero _) + by rw [← coeIdeal_bot, Ne, coeIdeal_inj]; rintro rfl; exact hI (dvd_zero _) have hJ' : (J : FractionalIdeal R⁰ K) ≠ 0 := - by rw [← coeIdeal_bot, Ne.def, coeIdeal_inj]; rintro rfl; exact hJ (dvd_zero _) + by rw [← coeIdeal_bot, Ne, coeIdeal_inj]; rintro rfl; exact hJ (dvd_zero _) have : ∀ n : ℕ, (1 ≤ n) → ¬∃ a b : R, ¬(x ^ n ∣ a) ∧ ¬(x ^ n ∣ b) ∧ spanSingleton R⁰ (algebraMap R K a / algebraMap R K b) = I / J := by intro n hn @@ -169,7 +169,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD ← mul_div_right_comm, eq_div_iff hJ', ← coeIdeal_span_singleton, ← coeIdeal_span_singleton, ← coeIdeal_mul, ← coeIdeal_mul, coeIdeal_inj] at e on_goal 2 => - rw [Ne.def, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero, + rw [Ne, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff] rintro rfl apply hb (dvd_zero _) @@ -180,7 +180,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD rwa [Irreducible.gcd_eq_one_iff] · rwa [irreducible_iff_prime, Ideal.prime_iff_isPrime, Ideal.span_singleton_prime] · exact hx.ne_zero - · rw [Ne.def, Ideal.span_singleton_eq_bot] + · rw [Ne, Ideal.span_singleton_eq_bot] exact hx.ne_zero rw [← Ideal.mem_span_singleton, ← Ideal.dvd_span_singleton] at ha' ⊢ replace h := ha'.trans (dvd_mul_right _ J) @@ -190,7 +190,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD rw [pow_succ', mul_dvd_mul_iff_left hx.ne_zero] at ha hb rw [_root_.map_mul, _root_.map_mul, mul_div_mul_left] at e₀ · exact IH ⟨a', b', ha, hb, e₀⟩ - · rw [Ne.def, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff] + · rw [Ne, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff] exact hx.ne_zero · refine IH ⟨a, b, h, ?_, e₀⟩ intro hb @@ -202,7 +202,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd, Irreducible.gcd_eq_one_iff] · rwa [irreducible_iff_prime, Ideal.prime_iff_isPrime, Ideal.span_singleton_prime] · exact hx.ne_zero - · rw [Ne.def, Ideal.span_singleton_eq_bot] + · rw [Ne, Ideal.span_singleton_eq_bot] exact hx.ne_zero · rwa [Nat.pos_iff_ne_zero, ← Nat.one_le_iff_ne_zero] rwa [← e, mul_comm, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at hb diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 952d31a7..126aeb12 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -721,9 +721,7 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E / intro i induction i with | zero => - simp only [Nat.zero_eq, zero_add, pow_one, map_inv₀, AlgEquiv.commutes] - rw [hE] - simp + simp only [pow_zero, AlgEquiv.one_apply, one_mul] | succ n ih => rw [pow_succ', AlgEquiv.mul_apply, ih, pow_succ'] simp only [inv_pow, map_mul, map_inv₀, map_pow, AlgEquiv.commutes] @@ -744,7 +742,7 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E / · simp -attribute [-instance] instDecidableEq Fintype.decidableForallFintype +attribute [-instance] Fintype.decidableForallFintype lemma unit_to_U_pow (x) (n : ℕ) : mkG (x ^ n) = n • (mkG x) := by induction n with | zero => simp [unit_to_U_one] diff --git a/FltRegular/NumberTheory/Hilbert94.lean b/FltRegular/NumberTheory/Hilbert94.lean index 9f1cf6bc..0f4d2fe7 100644 --- a/FltRegular/NumberTheory/Hilbert94.lean +++ b/FltRegular/NumberTheory/Hilbert94.lean @@ -9,7 +9,7 @@ open scoped NumberField variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] variable [Fintype (ClassGroup (𝓞 K))] -attribute [-instance] instCoeOut +-- attribute [-instance] instCoeOut open Polynomial diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean index ac8d37e9..19c70a81 100644 --- a/FltRegular/NumberTheory/KummersLemma/Field.lean +++ b/FltRegular/NumberTheory/KummersLemma/Field.lean @@ -12,7 +12,7 @@ variable (hp : p ≠ 2) variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (𝓞 K)ˣ) (hcong : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑u : 𝓞 K) - 1) (hu : ∀ v : K, v ^ (p : ℕ) ≠ u) -attribute [-instance] instCoeOut +-- attribute [-instance] instCoeOut open Polynomial diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean index 44897b1b..26466502 100644 --- a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean +++ b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean @@ -9,7 +9,7 @@ variable (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))] (hreg : (p : ℕ).Coprim variable {ζ : K} (hζ : IsPrimitiveRoot ζ p) (u : (𝓞 K)ˣ) (hcong : (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (↑u : 𝓞 K) - 1) (hu : ∀ v : K, v ^ (p : ℕ) ≠ u) -attribute [-instance] instCoeOut +-- attribute [-instance] instCoeOut open Polynomial From a51804506eb0a26691fff6cb4f5a7b4f5be65d8e Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 2 May 2024 21:15:05 +0200 Subject: [PATCH 3/6] more --- FltRegular/CaseII/InductionStep.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean index 3d4364e8..23551bdd 100644 --- a/FltRegular/CaseII/InductionStep.lean +++ b/FltRegular/CaseII/InductionStep.lean @@ -17,7 +17,7 @@ attribute [local instance 2000] Algebra.toModule Module.toDistribMulAction AddMo Semiring.toNonUnitalSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toMulZeroClass MulZeroClass.toMul Submodule.idemSemiring IdemSemiring.toSemiring - Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule + Submodule.instIdemCommSemiring IdemCommSemiring.toCommSemiring CommSemiring.toCommMonoid set_option quotPrecheck false @@ -80,7 +80,7 @@ lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) : ring apply Associated.mul_left apply hζ.unit'_coe.associated_sub_one hpri.out η₁.prop η₂.prop - rw [Ne.def, ← Subtype.ext_iff.not] + rw [Ne, ← Subtype.ext_iff.not] exact hη set_option synthInstance.maxHeartbeats 40000 in @@ -98,7 +98,7 @@ lemma div_zeta_sub_one_Injective : instance : Finite (𝓞 K ⧸ 𝔭) := by haveI : Fact (Nat.Prime p) := hpri letI := IsCyclotomicExtension.numberField {p} ℚ K - rw [← Ideal.absNorm_ne_zero_iff, Ne.def, Ideal.absNorm_eq_zero_iff, Ideal.span_singleton_eq_bot] + rw [← Ideal.absNorm_ne_zero_iff, Ne, Ideal.absNorm_eq_zero_iff, Ideal.span_singleton_eq_bot] exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt lemma div_zeta_sub_one_Bijective : @@ -155,14 +155,14 @@ lemma m_mul_c_mul_p : 𝔪 * 𝔠 η * 𝔭 = 𝔦 η := by set_option synthInstance.maxHeartbeats 40000 in lemma m_ne_zero : 𝔪 ≠ 0 := by - simp_rw [Ne.def, gcd_eq_zero_iff, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] + simp_rw [Ne, gcd_eq_zero_iff, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] rintro ⟨rfl, rfl⟩ exact hy (dvd_zero _) set_option synthInstance.maxHeartbeats 40000 in lemma p_ne_zero : 𝔭 ≠ 0 := by letI := IsCyclotomicExtension.numberField {p} ℚ K - rw [Ne.def, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] + rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] exact hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt lemma coprime_c_aux (η₁ η₂ : nthRootsFinset p (𝓞 K)) (hη : η₁ ≠ η₂) : (𝔦 η₁) ⊔ (𝔦 η₂) ∣ 𝔪 * 𝔭 := by @@ -232,7 +232,7 @@ lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = ( lemma exists_ideal_pow_eq_c : ∃ I : Ideal (𝓞 K), (𝔠 η) = I ^ (p : ℕ) := by letI inst1 : @IsDomain (Ideal (𝓞 K)) CommSemiring.toSemiring := @Ideal.isDomain (𝓞 K) _ _ - letI inst2 := @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero (𝓞 K) _ _ + letI inst2 := @Ideal.instNormalizedGCDMonoid (𝓞 K) _ _ letI inst3 := @NormalizedGCDMonoid.toGCDMonoid _ _ inst2 exact @Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (nthRootsFinset p (𝓞 K)) (Ideal (𝓞 K)) _ (by convert inst1) (by convert inst3) _ _ _ _ _ From d5c45ddec8cafd6db56125dbd3cf42a75b442532 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 2 May 2024 21:23:24 +0200 Subject: [PATCH 4/6] more --- FltRegular/CaseII/InductionStep.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean index 23551bdd..d928152f 100644 --- a/FltRegular/CaseII/InductionStep.lean +++ b/FltRegular/CaseII/InductionStep.lean @@ -401,7 +401,7 @@ lemma a_mul_denom_eq_a_zero_mul_num (hη : η ≠ η₀) : apply not_p_div_a_zero hp hζ e hy hz rw [ha] exact dvd_zero _ - · rw [Ne.def, FractionalIdeal.spanSingleton_eq_zero_iff, ← (algebraMap (𝓞 K) K).map_zero, + · rw [Ne, FractionalIdeal.spanSingleton_eq_zero_iff, ← (algebraMap (𝓞 K) K).map_zero, (IsFractionRing.injective (𝓞 K) K).eq_iff] intro hβ apply a_div_a_zero_denom_spec hp hreg hζ e hy hz η hη @@ -469,20 +469,20 @@ lemma exists_solution : have hη₁ : η₁ ≠ η₀ := by rw [← Subtype.coe_injective.ne_iff] show (η₀ * hζ.unit' : 𝓞 K) ≠ η₀ - rw [Ne.def, mul_right_eq_self₀, not_or] + rw [Ne, mul_right_eq_self₀, not_or] exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt, ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩ have hη₂ : η₂ ≠ η₀ := by rw [← Subtype.coe_injective.ne_iff] show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀ - rw [Ne.def, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or] + rw [Ne, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or] exact ⟨hζ.unit'_coe.pow_ne_one_of_pos_of_lt zero_lt_two (hpri.out.two_le.lt_or_eq.resolve_right (PNat.coe_injective.ne hp.symm)), ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩ have hη : η₂ ≠ η₁ := by rw [← Subtype.coe_injective.ne_iff] show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀ * hζ.unit' - rw [Ne.def, mul_right_eq_self₀, not_or] + rw [Ne, mul_right_eq_self₀, not_or] exact ⟨hζ.unit'_coe.ne_one hpri.out.one_lt, mul_ne_zero (ne_zero_of_mem_nthRootsFinset (η₀ : _).prop) (hζ.unit'_coe.ne_zero hpri.out.ne_zero)⟩ From 55474cbfceea969ded54d5f2bdbed5cfe1252fd0 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 2 May 2024 21:33:41 +0200 Subject: [PATCH 5/6] more --- FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean index 57027d33..c6b55514 100644 --- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean +++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean @@ -151,11 +151,11 @@ instance : Algebra (𝓞 K) (𝓞 K ⧸ I) := Ideal.Quotient.algebra _ instance : AddCommMonoid (𝓞 K) := inferInstance instance : AddCommMonoid (𝓞 K ⧸ I) := inferInstance +set_option synthInstance.maxHeartbeats 40000 in theorem aux {t} {l : 𝓞 K} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot μ p) (h : ∑ x : Fin t, f x • (⟨μ, hμ.isIntegral p.pos⟩ : 𝓞 K) ^ (x : ℕ) = l) : algebraMap (𝓞 K) (𝓞 K ⧸ I) l = ∑ x : Fin t, (f x : 𝓞 K ⧸ I) := by apply_fun algebraMap (𝓞 K) (𝓞 K ⧸ I) at h - stop simp only [map_sum, map_zsmul] at h convert h.symm using 1 congr From a602a91b176db0a1293ead2268b2d41d73610e89 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 2 May 2024 21:58:45 +0200 Subject: [PATCH 6/6] fix --- FltRegular/NumberTheory/Unramified.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean index 9dce864e..5b48bba5 100644 --- a/FltRegular/NumberTheory/Unramified.lean +++ b/FltRegular/NumberTheory/Unramified.lean @@ -164,6 +164,7 @@ lemma isUnramifiedAt_iff_SquareFree_minpoly_powerBasis [NoZeroSMulDivisors R S] open nonZeroDivisors Polynomial +set_option synthInstance.maxHeartbeats 40000 in attribute [local instance] Ideal.Quotient.field in lemma isUnramifiedAt_of_Separable_minpoly' [IsSeparable K L] (p : Ideal R) [hp : p.IsPrime] (hpbot : p ≠ ⊥) (x : S) @@ -195,6 +196,7 @@ lemma isUnramifiedAt_of_Separable_minpoly' [IsSeparable K L] have := hp.isMaximal hpbot intro P hP + letI : IsScalarTower S (S ⧸ P) (S ⧸ P) := IsScalarTower.right have := isMaximal_of_mem_primesOver hpbot hP apply le_antisymm · rw [← tsub_eq_zero_iff_le] @@ -211,11 +213,9 @@ lemma isUnramifiedAt_of_Separable_minpoly' [IsSeparable K L] rw [map_map, Ideal.quotientMap_comp_mk] at this obtain ⟨a, b, e⟩ := this apply_fun (aeval (Ideal.Quotient.mk P x)) at e - simp only [← Ideal.Quotient.algebraMap_eq, ← map_map, derivative_map, map_add, map_mul, - aeval_map_algebraMap, aeval_algebraMap_apply, minpoly.aeval, map_zero, mul_zero, hxP, - zero_add, coe_aeval_eq_eval, eval_one] at e - stop - exact zero_ne_one e + simp_rw [← Ideal.Quotient.algebraMap_eq, ← map_map, derivative_map, map_add, map_mul, + aeval_map_algebraMap, aeval_algebraMap_apply, minpoly.aeval, hxP, map_zero, mul_zero, + zero_add, map_one, zero_ne_one] at e · rwa [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _ (isMaximal_of_mem_primesOver hpbot hP).isPrime (ne_bot_of_mem_primesOver hpbot hP), Multiset.one_le_count_iff_mem, ← Multiset.mem_toFinset, ← primesOverFinset,