bump to nightly-2024-01-01-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean

@@ -160,14 +160,14 @@ varies over the `n`-th roots of unity. -/
 theorem X_pow_sub_one_eq_prod {ζ : R} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
     X ^ n - 1 = ∏ ζ in nthRootsFinset n R, (X - C ζ) :=
   by
-  rw [nth_roots_finset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_nodup h)]
+  rw [nth_roots_finset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_one_nodup h)]
   simp only [Finset.prod_mk, RingHom.map_one]
   rw [nth_roots]
   have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
   symm
   apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
   rw [@nat_degree_X_pow_sub_C R _ _ n 1, ← nth_roots]
-  exact IsPrimitiveRoot.card_nthRoots h
+  exact IsPrimitiveRoot.card_nthRoots_one h
 #align polynomial.X_pow_sub_one_eq_prod Polynomial.X_pow_sub_one_eq_prod
 -/
 
@@ -191,7 +191,8 @@ theorem cyclotomic'_splits (n : ℕ) : Splits (RingHom.id K) (cyclotomic' n K) :
 /-- If there is a primitive `n`-th root of unity in `K`, then `X ^ n - 1`splits. -/
 theorem X_pow_sub_one_splits {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
     Splits (RingHom.id K) (X ^ n - C (1 : K)) := by
-  rw [splits_iff_card_roots, ← nth_roots, IsPrimitiveRoot.card_nthRoots h, nat_degree_X_pow_sub_C]
+  rw [splits_iff_card_roots, ← nth_roots, IsPrimitiveRoot.card_nthRoots_one h,
+    nat_degree_X_pow_sub_C]
 #align polynomial.X_pow_sub_one_splits Polynomial.X_pow_sub_one_splits
 -/
 

Mathbin/RingTheory/RootsOfUnity/Basic.lean

@@ -995,10 +995,11 @@ theorem card_rootsOfUnity {ζ : R} {n : ℕ+} (h : IsPrimitiveRoot ζ n) :
 #align is_primitive_root.card_roots_of_unity IsPrimitiveRoot.card_rootsOfUnity
 -/
 
-#print IsPrimitiveRoot.card_nthRoots /-
+#print IsPrimitiveRoot.card_nthRoots_one /-
 /-- The cardinality of the multiset `nth_roots ↑n (1 : R)` is `n`
 if there is a primitive root of unity in `R`. -/
-theorem card_nthRoots {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRoots n (1 : R)).card = n :=
+theorem card_nthRoots_one {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
+    (nthRoots n (1 : R)).card = n :=
   by
   cases' Nat.eq_zero_or_pos n with hzero hpos
   · simp only [hzero, Multiset.card_zero, nth_roots_zero]
@@ -1013,13 +1014,13 @@ theorem card_nthRoots {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRoots
     set m := Nat.toPNat' n
     rw [← Fintype.card_congr (rootsOfUnityEquivNthRoots R m), card_rootsOfUnity h] at hcard 
     exact hcard
-#align is_primitive_root.card_nth_roots IsPrimitiveRoot.card_nthRoots
+#align is_primitive_root.card_nth_roots IsPrimitiveRoot.card_nthRoots_one
 -/
 
-#print IsPrimitiveRoot.nthRoots_nodup /-
+#print IsPrimitiveRoot.nthRoots_one_nodup /-
 /-- The multiset `nth_roots ↑n (1 : R)` has no repeated elements
 if there is a primitive root of unity in `R`. -/
-theorem nthRoots_nodup {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRoots n (1 : R)).Nodup :=
+theorem nthRoots_one_nodup {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRoots n (1 : R)).Nodup :=
   by
   cases' Nat.eq_zero_or_pos n with hzero hpos
   · simp only [hzero, Multiset.nodup_zero, nth_roots_zero]
@@ -1040,7 +1041,7 @@ theorem nthRoots_nodup {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (nthRoots
     set m := Nat.toPNat' n
     rw [hrw, ← Fintype.card_congr (rootsOfUnityEquivNthRoots R m), card_rootsOfUnity h] at ha 
     exact Nat.lt_asymm ha ha
-#align is_primitive_root.nth_roots_nodup IsPrimitiveRoot.nthRoots_nodup
+#align is_primitive_root.nth_roots_nodup IsPrimitiveRoot.nthRoots_one_nodup
 -/
 
 #print IsPrimitiveRoot.card_nthRootsFinset /-

lake-manifest.json

@@ -49,19 +49,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "3286beabe5f3da3a4d214f0f63b554fec8c40750",
+   "rev": "3694e27d9d9a84a7fc36ef5838cc33183af00403",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "3286beabe5f3da3a4d214f0f63b554fec8c40750",
+   "inputRev": "3694e27d9d9a84a7fc36ef5838cc33183af00403",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "dcc74ffa902f18b6693f389f21eeb4fbd772d2cf",
+   "rev": "c19c94c9b57be4d4ca1504c36222190d8b5ab140",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "dcc74ffa902f18b6693f389f21eeb4fbd772d2cf",
+   "inputRev": "c19c94c9b57be4d4ca1504c36222190d8b5ab140",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-12-31-06"
+def tag : String := "nightly-2024-01-01-06"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"dcc74ffa902f18b6693f389f21eeb4fbd772d2cf"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c19c94c9b57be4d4ca1504c36222190d8b5ab140"
 
 @[default_target]
 lean_lib Mathbin where