From 0309e0855ce7ee70839bca588e5f8764f7f5cc0a Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Wed, 31 Jul 2024 11:03:45 +0200 Subject: [PATCH] bump --- FltRegular/NumberTheory/Cyclotomic/CyclRat.lean | 4 ++-- FltRegular/NumberTheory/Hilbert90.lean | 8 ++++---- FltRegular/NumberTheory/Hilbert92.lean | 2 +- FltRegular/NumberTheory/SystemOfUnits.lean | 2 +- lake-manifest.json | 10 +++++----- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean index fcbfb463..b626bfd2 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean @@ -365,7 +365,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} 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 + Int.cast_smul_eq_nsmul] at hy obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.castOrderIso hdim.symm) ⟨i, hi⟩) y m rw [hn] at hy simp only [Fin.castOrderIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Hi, zero_sub, @@ -418,7 +418,7 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri 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] + rw [hy, ← smul_eq_mul, Int.cast_smul_eq_nsmul, ← b.basis.coord_apply, ← Fin.cast_mk, hn] exact dvd_add (dvd_mul_right _ _) last_dvd end IntFacts diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean index ddbdd4e1..92e08164 100644 --- a/FltRegular/NumberTheory/Hilbert90.lean +++ b/FltRegular/NumberTheory/Hilbert90.lean @@ -28,7 +28,7 @@ lemma hφ : ∀ (n : ℕ), φ σ ⟨σ ^ n, hσ _⟩ = n % (orderOf σ) := fun n noncomputable def cocycle : (L ≃ₐ[K] L) → Lˣ := fun τ ↦ ∏ i in range (φ σ ⟨τ, hσ τ⟩), Units.map (σ ^ i) (ηu hη) -lemma aux {a: ℕ} (h : a % orderOf σ = 0) : +lemma aux1 {a: ℕ} (h : a % orderOf σ = 0) : ∏ i in range a, (σ ^ i) (ηu hη) = 1 := by obtain ⟨n, hn⟩ := (Nat.dvd_iff_mod_eq_zero _ _).2 h rw [hn] @@ -53,14 +53,14 @@ lemma aux {a: ℕ} (h : a % orderOf σ = 0) : simp only [SetLike.coe_sort_coe, Subtype.coe_eta, Equiv.symm_apply_apply] rfl -lemma aux1 {a b : ℕ} (h : a % orderOf σ = b % orderOf σ) : +lemma aux2 {a b : ℕ} (h : a % orderOf σ = b % orderOf σ) : ∏ i in range a, (σ ^ i) (ηu hη) = ∏ i in range b, (σ ^ i) (ηu hη) := by wlog hab : b ≤ a generalizing a b · exact (this h.symm (not_le.1 hab).le).symm obtain ⟨c, hc⟩ := (Nat.dvd_iff_mod_eq_zero _ _).2 (Nat.sub_mod_eq_zero_of_mod_eq h) rw [Nat.sub_eq_iff_eq_add hab] at hc rw [hc, prod_range_add] - rw [aux hσ hη (Nat.mul_mod_right (orderOf σ) c), one_mul] + rw [aux1 hσ hη (Nat.mul_mod_right (orderOf σ) c), one_mul] simp [pow_add, pow_mul, pow_orderOf_eq_one] lemma cocycle_spec (hone : orderOf σ ≠ 1) : (cocycle hσ hη) σ = (ηu hη) := by @@ -104,7 +104,7 @@ lemma is_cocycle_aux : ∀ (α β : (L ≃ₐ[K] L)), (cocycle hσ hη) (α * β enter [2, 2, 2, x] rw [← AlgEquiv.mul_apply, ← pow_add, H] rw [← prod_range_add (fun (n : ℕ) ↦ (σ ^ n) (ηu hη)) (a % orderOf σ) (b % orderOf σ)] - simpa using aux1 hσ hη (by simp) + simpa using aux2 hσ hη (by simp) lemma is_cocycle : IsMulOneCocycle (cocycle hσ hη) := by intro α β diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 64097b3d..a8feb330 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -227,7 +227,7 @@ lemma corollary [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (a simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul, b', b] congr 1 · rw [mul_comm] - · rw [← intCast_smul (k := A), smul_smul] + · rw [← Int.cast_smul_eq_nsmul (R := A), smul_smul] · simp end systemOfUnits.IsFundamental diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean index 0e73fe86..89764200 100644 --- a/FltRegular/NumberTheory/SystemOfUnits.lean +++ b/FltRegular/NumberTheory/SystemOfUnits.lean @@ -79,7 +79,7 @@ lemma existence' [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) : replace hy := congr_arg (f • ·) hy simp only at hy rw [smul_zero, smul_add, smul_smul, mul_comm f, - ← Hf, ← eq_neg_iff_add_eq_zero, intCast_smul] at hy + ← Hf, ← eq_neg_iff_add_eq_zero, Int.cast_smul_eq_nsmul] at hy apply hg _ h0 rw [hy] exact Submodule.neg_mem _ (Submodule.smul_mem _ _ y.2) diff --git a/lake-manifest.json b/lake-manifest.json index ccad52c8..529fbaf5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592", + "rev": "3dfb59cffd1fdeaa41a92588c0d57e9a70cba8b6", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "79fb157c6a5061190d169535f8e5cb007914a82e", + "rev": "9c66fa5071dba9578bb20a3bade04bcc15c57fc2", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "c87908619cccadda23f71262e6898b9893bffa36", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.40", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "75defd205f298e1b8d4197cc1b81c598f01000d6", + "rev": "1aef8600a6550e8de3bc501d66cfa5fe56f20b76", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,