bump to nightly-2023-10-12-06

mathlib commit leanprover-community/mathlib@19c869e
leanprover-community · Oct 12, 2023 · 1958166 · 1958166
1 parent 6e6bbb7
commit 1958166
Show file tree

Hide file tree

Showing 9 changed files with 19 additions and 19 deletions.
diff --git a/Archive/All.lean b/Archive/All.lean
@@ -53,5 +53,5 @@ import Wiedijk100Theorems.PerfectNumbers
 import Wiedijk100Theorems.SolutionOfCubic
 import Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 
-#align_import all from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
+#align_import all from "leanprover-community/mathlib"@"19c869efa56bbb8b500f2724c0b77261edbfa28c"
 
diff --git a/Counterexamples/All.lean b/Counterexamples/All.lean
@@ -13,5 +13,5 @@ import SeminormLatticeNotDistrib
 import SorgenfreyLine
 import ZeroDivisorsInAddMonoidAlgebras
 
-#align_import all from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
+#align_import all from "leanprover-community/mathlib"@"19c869efa56bbb8b500f2724c0b77261edbfa28c"
 
diff --git a/Mathbin/All.lean b/Mathbin/All.lean
@@ -3218,5 +3218,5 @@ import Topology.VectorBundle.Basic
 import Topology.VectorBundle.Constructions
 import Topology.VectorBundle.Hom
 
-#align_import all from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"
+#align_import all from "leanprover-community/mathlib"@"19c869efa56bbb8b500f2724c0b77261edbfa28c"
 
diff --git a/Mathbin/RingTheory/Artinian.lean b/Mathbin/RingTheory/Artinian.lean
@@ -244,11 +244,11 @@ theorem induction {P : Submodule R M → Prop} (hgt : ∀ I, (∀ J < I, P J)
 #align is_artinian.induction IsArtinian.induction
 -/
 
-#print IsArtinian.exists_endomorphism_iterate_ker_sup_range_eq_top /-
+#print LinearMap.eventually_codisjoint_ker_pow_range_pow /-
 /-- For any endomorphism of a Artinian module, there is some nontrivial iterate
 with disjoint kernel and range.
 -/
-theorem exists_endomorphism_iterate_ker_sup_range_eq_top (f : M →ₗ[R] M) :
+theorem eventually_codisjoint_ker_pow_range_pow (f : M →ₗ[R] M) :
     ∃ n : ℕ, n ≠ 0 ∧ (f ^ n).ker ⊔ (f ^ n).range = ⊤ :=
   by
   obtain ⟨n, w⟩ :=
@@ -266,7 +266,7 @@ theorem exists_endomorphism_iterate_ker_sup_range_eq_top (f : M →ₗ[R] M) :
     simp [iterate_add_apply]
   · use(f ^ (n + 1)) y
     simp
-#align is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top IsArtinian.exists_endomorphism_iterate_ker_sup_range_eq_top
+#align is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top LinearMap.eventually_codisjoint_ker_pow_range_pow
 -/
 
 #print IsArtinian.surjective_of_injective_endomorphism /-

diff --git a/Mathbin/RingTheory/Noetherian.lean b/Mathbin/RingTheory/Noetherian.lean
@@ -428,12 +428,12 @@ theorem isNoetherian_of_range_eq_ker [IsNoetherian R M] [IsNoetherian R P] (f :
 #align is_noetherian_of_range_eq_ker isNoetherian_of_range_eq_ker
 -/
 
-#print IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot /-
+#print LinearMap.eventually_disjoint_ker_pow_range_pow /-
 /-- For any endomorphism of a Noetherian module, there is some nontrivial iterate
 with disjoint kernel and range.
 -/
-theorem IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot [I : IsNoetherian R M]
-    (f : M →ₗ[R] M) : ∃ n : ℕ, n ≠ 0 ∧ (f ^ n).ker ⊓ (f ^ n).range = ⊥ :=
+theorem LinearMap.eventually_disjoint_ker_pow_range_pow [I : IsNoetherian R M] (f : M →ₗ[R] M) :
+    ∃ n : ℕ, n ≠ 0 ∧ (f ^ n).ker ⊓ (f ^ n).range = ⊥ :=
   by
   obtain ⟨n, w⟩ :=
     monotone_stabilizes_iff_noetherian.mpr I
@@ -449,15 +449,15 @@ theorem IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot [I : IsNoe
   rw [← pow_add] at h 
   convert h using 3
   ring
-#align is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot
+#align is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot LinearMap.eventually_disjoint_ker_pow_range_pow
 -/
 
 #print IsNoetherian.injective_of_surjective_endomorphism /-
 /-- Any surjective endomorphism of a Noetherian module is injective. -/
 theorem IsNoetherian.injective_of_surjective_endomorphism [IsNoetherian R M] (f : M →ₗ[R] M)
     (s : Surjective f) : Injective f :=
   by
-  obtain ⟨n, ne, w⟩ := IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot f
+  obtain ⟨n, ne, w⟩ := LinearMap.eventually_disjoint_ker_pow_range_pow f
   rw [linear_map.range_eq_top.mpr (LinearMap.iterate_surjective s n), inf_top_eq,
     LinearMap.ker_eq_bot] at w 
   exact LinearMap.injective_of_iterate_injective Ne w

diff --git a/README.md b/README.md
@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`c8f305514e0d47dfaa710f5a52f0d21b588e6328`](https://github.com/leanprover-community/mathlib/commit/c8f305514e0d47dfaa710f5a52f0d21b588e6328)
+Tracking mathlib commit: [`19c869efa56bbb8b500f2724c0b77261edbfa28c`](https://github.com/leanprover-community/mathlib/commit/19c869efa56bbb8b500f2724c0b77261edbfa28c)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "065336f66d9d62bcb86f79b2635ecabaf8918b06",
+    "rev": "9c0d65b881440ef8437205319f3d7096ea6d0895",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "065336f66d9d62bcb86f79b2635ecabaf8918b06",
+    "inputRev?": "9c0d65b881440ef8437205319f3d7096ea6d0895",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "3f4910debcdd03d6ca9f9063b698a36fd2e3c211",
+    "rev": "ad5f24375827ac0d93c6f37f446bede116af2f4b",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "3f4910debcdd03d6ca9f9063b698a36fd2e3c211",
+    "inputRev?": "ad5f24375827ac0d93c6f37f446bede116af2f4b",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",

diff --git a/lakefile.lean b/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-10-11-06"
+def tag : String := "nightly-2023-10-12-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"@"065336f66d9d62bcb86f79b2635ecabaf8918b06"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"9c0d65b881440ef8437205319f3d7096ea6d0895"
 
 @[default_target]
 lean_lib Mathbin where

diff --git a/upstream-rev b/upstream-rev
@@ -1 +1 @@
-c8f305514e0d47dfaa710f5a52f0d21b588e6328
+19c869efa56bbb8b500f2724c0b77261edbfa28c