bump to nightly-2023-03-09-14

mathlib commit leanprover-community/mathlib@21e3562

Mathbin/Algebra/Polynomial/GroupRingAction.lean

@@ -102,7 +102,7 @@ noncomputable def prodXSubSmul (x : R) : R[X] :=
 #align prod_X_sub_smul prodXSubSmul
 
 theorem prodXSubSmul.monic (x : R) : (prodXSubSmul G R x).Monic :=
-  Polynomial.monic_prod_of_monic _ _ fun g _ => Polynomial.monic_x_sub_c _
+  Polynomial.monic_prod_of_monic _ _ fun g _ => Polynomial.monic_X_sub_C _
 #align prod_X_sub_smul.monic prodXSubSmul.monic
 
 theorem prodXSubSmul.eval (x : R) : (prodXSubSmul G R x).eval x = 0 :=

Mathbin/Data/Polynomial/Div.lean

@@ -564,7 +564,7 @@ def rootMultiplicity (a : R) (p : R[X]) : ℕ :=
   if h0 : p = 0 then 0
   else
     let I : DecidablePred fun n : ℕ => ¬(X - C a) ^ (n + 1) ∣ p := fun n =>
-      @Not.decidable _ (decidableDvdMonic p ((monic_x_sub_c a).pow (n + 1)))
+      @Not.decidable _ (decidableDvdMonic p ((monic_X_sub_C a).pow (n + 1)))
     Nat.find (multiplicity_X_sub_C_finite a h0)
 #align polynomial.root_multiplicity Polynomial.rootMultiplicity
 
@@ -614,7 +614,7 @@ theorem pow_rootMultiplicity_dvd (p : R[X]) (a : R) : (X - C a) ^ rootMultiplici
 theorem divByMonic_mul_pow_rootMultiplicity_eq (p : R[X]) (a : R) :
     p /ₘ (X - C a) ^ rootMultiplicity a p * (X - C a) ^ rootMultiplicity a p = p :=
   by
-  have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_x_sub_c _).pow _
+  have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
   conv_rhs =>
       rw [← mod_by_monic_add_div p this,
         (dvd_iff_mod_by_monic_eq_zero this).2 (pow_root_multiplicity_dvd _ _)] <;>

Mathbin/Data/Polynomial/FieldDivision.lean

@@ -215,11 +215,11 @@ theorem divByMonic_eq_div (p : R[X]) (hq : Monic q) : p /ₘ q = p / q :=
 #align polynomial.div_by_monic_eq_div Polynomial.divByMonic_eq_div
 
 theorem mod_x_sub_c_eq_c_eval (p : R[X]) (a : R) : p % (X - C a) = C (p.eval a) :=
-  modByMonic_eq_mod p (monic_x_sub_c a) ▸ modByMonic_x_sub_c_eq_c_eval _ _
+  modByMonic_eq_mod p (monic_X_sub_C a) ▸ modByMonic_x_sub_c_eq_c_eval _ _
 #align polynomial.mod_X_sub_C_eq_C_eval Polynomial.mod_x_sub_c_eq_c_eval
 
 theorem mul_div_eq_iff_isRoot : (X - C a) * (p / (X - C a)) = p ↔ IsRoot p a :=
-  divByMonic_eq_div p (monic_x_sub_c a) ▸ mul_divByMonic_eq_iff_isRoot
+  divByMonic_eq_div p (monic_X_sub_C a) ▸ mul_divByMonic_eq_iff_isRoot
 #align polynomial.mul_div_eq_iff_is_root Polynomial.mul_div_eq_iff_isRoot
 
 instance : EuclideanDomain R[X] :=

Mathbin/Data/Polynomial/RingDivision.lean

@@ -1052,7 +1052,7 @@ theorem pairwise_coprime_x_sub_c {K} [Field K] {I : Type v} {s : I → K} (H : F
 #align polynomial.pairwise_coprime_X_sub_C Polynomial.pairwise_coprime_x_sub_c
 
 theorem monic_prod_multiset_x_sub_c : Monic (p.roots.map fun a => X - C a).Prod :=
-  monic_multiset_prod_of_monic _ _ fun a _ => monic_x_sub_c a
+  monic_multiset_prod_of_monic _ _ fun a _ => monic_X_sub_C a
 #align polynomial.monic_prod_multiset_X_sub_C Polynomial.monic_prod_multiset_x_sub_c
 
 theorem prod_multiset_root_eq_finset_root :

Mathbin/FieldTheory/Minpoly/Field.lean

@@ -271,7 +271,7 @@ theorem root {x : B} (hx : IsIntegral A x) {y : A} (h : IsRoot (minpoly A x) y)
     algebraMap A B y = x :=
   by
   have key : minpoly A x = X - C y :=
-    eq_of_monic_of_associated (monic hx) (monic_x_sub_c y)
+    eq_of_monic_of_associated (monic hx) (monic_X_sub_C y)
       (associated_of_dvd_dvd
         ((irreducible_x_sub_c y).dvd_symm (irreducible hx) (dvd_iff_isRoot.2 h))
         (dvd_iff_isRoot.2 h))

Mathbin/RingTheory/IntegralClosure.lean

@@ -79,7 +79,7 @@ protected def Algebra.IsIntegral : Prop :=
 variable {R A}
 
 theorem RingHom.is_integral_map {x : R} : f.IsIntegralElem (f x) :=
-  ⟨X - C x, monic_x_sub_c _, by simp⟩
+  ⟨X - C x, monic_X_sub_C _, by simp⟩
 #align ring_hom.is_integral_map RingHom.is_integral_map
 
 theorem isIntegral_algebraMap {x : R} : IsIntegral R (algebraMap R A x) :=

Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean

@@ -105,7 +105,7 @@ theorem cyclotomic'_two (R : Type _) [CommRing R] [IsDomain R] (p : ℕ) [CharP
 /-- `cyclotomic' n R` is monic. -/
 theorem cyclotomic'.monic (n : ℕ) (R : Type _) [CommRing R] [IsDomain R] :
     (cyclotomic' n R).Monic :=
-  monic_prod_of_monic _ _ fun z hz => monic_x_sub_c _
+  monic_prod_of_monic _ _ fun z hz => monic_X_sub_C _
 #align polynomial.cyclotomic'.monic Polynomial.cyclotomic'.monic
 
 /-- `cyclotomic' n R` is different from `0`. -/

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "da1463c8620c9fcc3d9a770aa52f0c5a66390c2e",
+    "rev": "9f7b25530726cbd5bfd6d1a93b5bde7b836a0426",
     "name": "lean3port",
-    "inputRev?": "da1463c8620c9fcc3d9a770aa52f0c5a66390c2e"}},
+    "inputRev?": "9f7b25530726cbd5bfd6d1a93b5bde7b836a0426"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "69108c782429c57637807f32d923e34c195ec823",
+    "rev": "0ee6690d078a47e95313b4a53c5dcfea78d8269e",
     "name": "mathlib",
-    "inputRev?": "69108c782429c57637807f32d923e34c195ec823"}},
+    "inputRev?": "0ee6690d078a47e95313b4a53c5dcfea78d8269e"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-03-09-12"
+def tag : String := "nightly-2023-03-09-14"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"da1463c8620c9fcc3d9a770aa52f0c5a66390c2e"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"9f7b25530726cbd5bfd6d1a93b5bde7b836a0426"
 
 @[default_target]
 lean_lib Mathbin where