bump

FltRegular/CaseI/Statement.lean

@@ -224,7 +224,7 @@ theorem caseI_easier {a b c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p)
     (hgcd : ({a, b, c} : Finset ℤ).gcd id = 1) (hab : ¬a ≡ b [ZMOD p]) (caseI : ¬↑p ∣ a * b * c) :
     a ^ p + b ^ p ≠ c ^ p := by
   have hcycl : IsCyclotomicExtension {P} ℤ (𝓞 (CyclotomicField P ℚ)) := by
-    apply @IsCyclotomicExtension.ring_of_integers' _ _ _ _ (by exact hpri) _
+    apply @IsCyclotomicExtension.ring_of_integers' _ _ _ (by exact hpri) _
   set ζ := zeta P ℤ R
   have hζ := zeta_spec P ℤ R
   intro H

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,
-    Int.cast_smul_eq_nsmul] at hy
+    Int.cast_smul_eq_zsmul] 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, Int.cast_smul_eq_nsmul, ← b.basis.coord_apply, ← Fin.cast_mk, hn]
+  rw [hy, ← smul_eq_mul, Int.cast_smul_eq_zsmul, ← b.basis.coord_apply, ← Fin.cast_mk, hn]
   exact dvd_add (dvd_mul_right _ _) last_dvd
 
 end IntFacts

FltRegular/NumberTheory/Hilbert92.lean

@@ -230,7 +230,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 [← Int.cast_smul_eq_nsmul (R := A), smul_smul]
+    · rw [← Int.cast_smul_eq_zsmul (R := A), smul_smul]
   · simp
 
 end systemOfUnits.IsFundamental
@@ -455,7 +455,6 @@ lemma unitlifts_spec (S : systemOfUnits p G (NumberField.Units.rank k + 1)) (i)
     mkG (Additive.toMul <| unitlifts p hp hKL σ hσ S i) = S.units i := by
   delta unit_to_U unitlifts
   simp only [toMul_ofMul, Quotient.out_eq', ofMul_toMul]
-  exact Quotient.out_eq' _
 
 lemma u_lemma2 (u v : (𝓞 K)ˣ) (hu : u = v / (σ v : K)) : (mkG u) = (1 - zeta p : A) • (mkG v) := by
   rw [sub_smul, one_smul, relativeUnitsModule_zeta_smul, ← unit_to_U_div]

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, Int.cast_smul_eq_nsmul] at hy
+      ← Hf, ← eq_neg_iff_add_eq_zero, Int.cast_smul_eq_zsmul] at hy
     apply hg _ h0
     rw [hy]
     exact Submodule.neg_mem _ (Submodule.smul_mem _ _ y.2)

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "41bc768e2224d6c75128a877f1d6e198859b3178",
+   "rev": "dc167d260ff7ee9849b436037add06bed15104be",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6058ab8d938c5104eace7d0fb5ac17b21cb067b1",
+   "rev": "0444234b4216e944d5be2ce42a25d7410c67876f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "10a631f1d3d9d99b990791ca0a251a5e78a15d84",
+   "rev": "ce6b0a984cb0cdf3d5915ec352d7f8f0d7a8af36",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "32c52a4b35ba8a3d261056e0d264de7bb94c062e",
+   "rev": "6d8e3118ab526f8dfcabcbdf9f05dc34e5c423a8",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0-rc1