From 5752bebd68d2abd548251ab6b485d4c0593f3509 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 30 May 2024 16:01:26 +0200 Subject: [PATCH] bump --- FltRegular/FltThree/FltThree.lean | 2 +- FltRegular/FltThree/Spts.lean | 6 ++--- FltRegular/MayAssume/Lemmas.lean | 2 +- .../NumberTheory/Cyclotomic/CyclRat.lean | 26 +++++++++---------- FltRegular/NumberTheory/Hilbert92.lean | 2 +- lake-manifest.json | 8 +++--- 6 files changed, 23 insertions(+), 23 deletions(-) diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean index 172567de..9ba3ad66 100644 --- a/FltRegular/FltThree/FltThree.lean +++ b/FltRegular/FltThree/FltThree.lean @@ -237,7 +237,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : exact dvd_mul_right _ _ · have h000 : d ∣ 3 * q.natAbs ^ 2 := by - rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.coe_nat_pow, Int.natAbs_sq, Nat.cast_three] + rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.natCast_pow, Int.natAbs_sq, Nat.cast_three] use Q - d * H ^ 2 rw [mul_sub, ← hQ, hp] ring diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean index dc674df3..96552d2a 100644 --- a/FltRegular/FltThree/Spts.lean +++ b/FltRegular/FltThree/Spts.lean @@ -67,7 +67,7 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime · set X : ℤ√(-3) := ⟨p.re * a.re - A * 3 * p.im * a.im, p.re * a.im + A * a.re * p.im⟩ with HX obtain ⟨U, HU⟩ : (p.norm : ℤ√(-3)) ∣ X := by - rw [Zsqrtd.coe_int_dvd_iff] + rw [Zsqrtd.intCast_dvd] refine' ⟨_, HA⟩ apply @Prime.dvd_of_dvd_pow _ _ _ hpprime _ 2 have : X.re ^ 2 = X.norm - 3 * X.im ^ 2 := @@ -282,8 +282,8 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod exact dvd_add (dvd_mul_of_dvd_left - ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _) - (dvd_mul_of_dvd_right ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr hpdvdright) _) + ((Zsqrtd.intCast_dvd_intCast _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _) + (dvd_mul_of_dvd_right ((Zsqrtd.intCast_dvd_intCast _ _).mpr hpdvdright) _) have := Zsqrtd.coprime_of_dvd_coprime hcoprime this simp only [Zsqrtd.intCast_re, isCoprime_zero_right, Zsqrtd.intCast_im, hpprime.not_unit] at this have h6 : x * z = C'.norm := by diff --git a/FltRegular/MayAssume/Lemmas.lean b/FltRegular/MayAssume/Lemmas.lean index 207afc38..9d39e67c 100644 --- a/FltRegular/MayAssume/Lemmas.lean +++ b/FltRegular/MayAssume/Lemmas.lean @@ -51,7 +51,7 @@ theorem p_dvd_c_of_ab_of_anegc {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp : p (h : a ^ p + b ^ p = c ^ p) (hab : a ≡ b [ZMOD p]) (hbc : b ≡ -c [ZMOD p]) : ↑p ∣ c := by letI : Fact p.Prime := ⟨hpri⟩ replace h := congr_arg (fun n : ℤ => (n : ZMod p)) h - simp only [Int.coe_nat_pow, Int.cast_add, Int.cast_pow, ZMod.pow_card] at h + simp only [Int.natCast_pow, Int.cast_add, Int.cast_pow, ZMod.pow_card] at h simp only [← ZMod.intCast_eq_intCast_iff, Int.cast_neg] at hbc hab rw [hab, hbc, ← sub_eq_zero, ← sub_eq_add_neg, ← Int.cast_neg, ← Int.cast_sub, ← Int.cast_sub] at h diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean index 6ebbb627..3279f436 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean @@ -336,9 +336,9 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} m ∣ f ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ := by obtain ⟨i, Hi⟩ := hf have hlast : - (Fin.castIso (succ_pred_prime hp.out)) (Fin.last (p : ℕ).pred) = + (Fin.castOrderIso (succ_pred_prime hp.out)) (Fin.last (p : ℕ).pred) = ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ := Fin.ext rfl - have h : ∀ x, (Fin.castIso (succ_pred_prime hp.out)) (Fin.castSuccEmb x) = + have h : ∀ x, (Fin.castOrderIso (succ_pred_prime hp.out)) (Fin.castSuccEmb x) = ⟨x, lt_trans x.2 (pred_lt hp.out.ne_zero)⟩ := fun x => Fin.ext rfl let ζ' := (ζ : L) have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ @@ -352,10 +352,10 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} by_contra! habs simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt i))] at H obtain ⟨y, hy⟩ := hdiv - rw [← Equiv.sum_comp (Fin.castIso (succ_pred_prime hp.out)).toEquiv, Fin.sum_univ_castSucc] at hy + rw [← Equiv.sum_comp (Fin.castOrderIso (succ_pred_prime hp.out)).toEquiv, Fin.sum_univ_castSucc] at hy simp only [hlast, h, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy rw [hζ.pow_sub_one_eq hp.out.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib, - ← (Fin.castIso hdim).toEquiv.sum_comp] at hy + ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy simp only [RelIso.coe_fn_toEquiv, Fin.coe_cast, mul_neg, ← Subtype.coe_inj, Fin.coe_castSucc, Fin.coe_orderIso_apply] at hy push_cast at hy @@ -371,13 +371,13 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg] norm_cast at hy rw [sum_sub_distrib] at hy - replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨i, hi⟩)) hy + replace hy := congr_arg (b.basis.coord ((Fin.castOrderIso hdim.symm) ⟨i, hi⟩)) hy rw [← b.basis.equivFun_symm_apply, ← b.basis.equivFun_symm_apply, LinearMap.map_sub, b.basis.coord_equivFun_symm, b.basis.coord_equivFun_symm, ← smul_eq_mul, ← zsmul_eq_smul_cast] at hy - obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.castIso hdim.symm) ⟨i, hi⟩) y m + obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.castOrderIso hdim.symm) ⟨i, hi⟩) y m rw [hn] at hy - simp only [Fin.castIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Hi, zero_sub, + simp only [Fin.castOrderIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Hi, zero_sub, neg_eq_iff_eq_neg] at hy erw [hy] -- pred vs - 1 simp [dvd_neg] @@ -389,9 +389,9 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri have : Fact (p : ℕ).Prime := ⟨hp⟩ have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by rfl - have hlast : (Fin.castIso (succ_pred_prime hp)) (Fin.last (p : ℕ).pred) = + have hlast : (Fin.castOrderIso (succ_pred_prime hp)) (Fin.last (p : ℕ).pred) = ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩ := Fin.ext rfl - have h : ∀ x, (Fin.castIso (succ_pred_prime hp)) (Fin.castSuccEmb x) = + have h : ∀ x, (Fin.castOrderIso (succ_pred_prime hp)) (Fin.castSuccEmb x) = ⟨x, lt_trans x.2 (pred_lt hp.ne_zero)⟩ := fun x => Fin.ext rfl set b := hζ'.integralPowerBasis' with hb have hdim : b.dim = (p : ℕ).pred := by rw [hζ'.power_basis_int'_dim, totient_prime hp, @@ -404,10 +404,10 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri by_contra! habs simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H obtain ⟨y, hy⟩ := hdiv - rw [← Equiv.sum_comp (Fin.castIso (succ_pred_prime hp)).toEquiv, Fin.sum_univ_castSucc] at hy + rw [← Equiv.sum_comp (Fin.castOrderIso (succ_pred_prime hp)).toEquiv, Fin.sum_univ_castSucc] at hy simp only [hlast, h, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy rw [hζ.pow_sub_one_eq hp.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib, - ← (Fin.castIso hdim).toEquiv.sum_comp] at hy + ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy simp only [RelIso.coe_fn_toEquiv, Fin.coe_cast, mul_neg, ← Subtype.coe_inj, Fin.coe_castSucc, Fin.coe_orderIso_apply] at hy push_cast at hy @@ -423,10 +423,10 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg] norm_cast at hy rw [sum_sub_distrib] at hy - replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨j, hj⟩)) hy + replace hy := congr_arg (b.basis.coord ((Fin.castOrderIso hdim.symm) ⟨j, hj⟩)) hy rw [← b.basis.equivFun_symm_apply, ← b.basis.equivFun_symm_apply, LinearMap.map_sub, b.basis.coord_equivFun_symm, b.basis.coord_equivFun_symm] at hy - simp only [Fin.castIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Basis.coord_apply, + simp only [Fin.castOrderIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Basis.coord_apply, sub_eq_iff_eq_add] at hy obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.cast hdim.symm) ⟨j, hj⟩) y m rw [hy, ← smul_eq_mul, ← zsmul_eq_smul_cast, ← b.basis.coord_apply, ← Fin.cast_mk, hn] diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index b8394d19..71e0e4b2 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -493,7 +493,7 @@ theorem padicValNat_dvd_iff' {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℕ) : theorem padicValInt_dvd_iff' {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℤ) : (p : ℤ) ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a := by rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff' hp, ← Int.natCast_dvd, - Int.coe_nat_pow] + Int.natCast_pow] theorem padicValInt_dvd' {p : ℕ} (a : ℤ) : (p : ℤ) ^ padicValInt p a ∣ a := by by_cases hp : p = 1 diff --git a/lake-manifest.json b/lake-manifest.json index 75904b9d..6926b8f2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06", + "rev": "60d622c124cebcecc000853cdae93f4251f4beb5", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236", + "rev": "70ec1d99be1e1b835d831f39c01b0d14921d2118", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb", + "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "5bf1683fbb7de26aee023022376acb23c740b3f5", + "rev": "dbaf55811cc1dd45a83c26c367094da1fe666707", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,