bump

leanprover-community · Jul 31, 2024 · 0309e08 · 0309e08
1 parent 015f73f
commit 0309e08
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 13 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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,