Updates available and ready to merge

FLT/MathlibExperiments/FrobeniusRiou.lean

@@ -11,7 +11,7 @@ import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.Over
 import Mathlib.FieldTheory.Normal
-import Mathlib
+import Mathlib.FieldTheory.SeparableClosure
 import Mathlib.RingTheory.OreLocalization.Ring
 
 /-!
@@ -527,10 +527,36 @@ theorem reduction_isIntegral
 
 end MulSemiringAction
 
-theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [CommRing S]
-    [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
-    ∃ r : R, r ≠ 0 ∧ s ∣ (r : S) := by
-  sorry
+theorem Polynomial.nonzero_const_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
+    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
+    ∃ (q : Polynomial R), q.coeff 0 ≠ 0 ∧ q.eval₂ (algebraMap R S) s = 0 := by
+  obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s
+  have p_nzero := ne_zero_of_ne_zero_of_monic X_ne_zero p_monic
+  obtain ⟨q, p_eq, q_ndvd⟩ := Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd p p_nzero 0
+  rw [C_0, sub_zero] at p_eq
+  rw [C_0, sub_zero] at q_ndvd
+  use q
+  constructor
+  . intro q_coeff_0
+    exact q_ndvd <| X_dvd_iff.mpr q_coeff_0
+  . rw [p_eq, eval₂_mul] at p_eval
+    rcases NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero p_eval with Xpow_eval | q_eval
+    . by_contra
+      apply hs
+      rw [eval₂_X_pow] at Xpow_eval
+      exact pow_eq_zero Xpow_eval
+    . exact q_eval
+
+theorem Algebra.exists_dvd_nonzero_if_isIntegral (R S : Type) [CommRing R] [Nontrivial R]
+    [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) :
+    ∃ r : R, r ≠ 0 ∧ s ∣ (algebraMap R S) r := by
+  obtain ⟨q, q_zero_coeff, q_eval_zero⟩ := Polynomial.nonzero_const_if_isIntegral R S s hs
+  use q.coeff 0
+  refine ⟨q_zero_coeff, ?_⟩
+  rw [← Polynomial.eval₂_X (algebraMap R S) s, ← dvd_neg, ← Polynomial.eval₂_C (algebraMap R S) s]
+  rw [← zero_add (-_), Mathlib.Tactic.RingNF.add_neg, ← q_eval_zero, ← Polynomial.eval₂_sub]
+  apply Polynomial.eval₂_dvd
+  exact Polynomial.X_dvd_sub_C
 
 end B_mod_Q_over_A_mod_P_stuff
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
+   "rev": "1e0bf50b357069e1d658512a579a5faac6587c40",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.43",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7376ac07aa2b0492372c056b7a2c3163b3026d1e",
+   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066",
+   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8a434b09e83db1785dbd4476134981712c606746",
+   "rev": "418a5eb7aec3fb639097cb13f74fc031ac4057f2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ccb4e97ffb7ad0f9b1852e9669d5e2922f984175",
+   "rev": "d36b7fd4c730cae8a3a8edfe98beb34ef0fc6e0a",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",