From 19581661e80bd3541d55a13909d4cfad5f9aabcb Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Thu, 12 Oct 2023 06:37:46 +0000 Subject: [PATCH] bump to nightly-2023-10-12-06 mathlib commit https://github.com/leanprover-community/mathlib/commit/19c869efa56bbb8b500f2724c0b77261edbfa28c --- Archive/All.lean | 2 +- Counterexamples/All.lean | 2 +- Mathbin/All.lean | 2 +- Mathbin/RingTheory/Artinian.lean | 6 +++--- Mathbin/RingTheory/Noetherian.lean | 10 +++++----- README.md | 2 +- lake-manifest.json | 8 ++++---- lakefile.lean | 4 ++-- upstream-rev | 2 +- 9 files changed, 19 insertions(+), 19 deletions(-) diff --git a/Archive/All.lean b/Archive/All.lean index 5a9e4c27b2..c1d115bb6f 100644 --- 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 index 16a8ded516..2fe48e651b 100644 --- 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 index 572f9e2490..3db5898cf2 100644 --- 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 index 9db6cbb701..449f0e484a 100644 --- 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 index f8701b6d0e..bbf6007b34 100644 --- 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,7 +449,7 @@ 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 /- @@ -457,7 +457,7 @@ theorem IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot [I : IsNoe 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 index 89d29b96cd..09df7aa970 100644 --- 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 index e91533a465..51aa38bfcf 100644 --- 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 index d14609d4ef..1b8ddabfcc 100644 --- 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 index 8fe90bf6db..4cae56e5af 100644 --- a/upstream-rev +++ b/upstream-rev @@ -1 +1 @@ -c8f305514e0d47dfaa710f5a52f0d21b588e6328 +19c869efa56bbb8b500f2724c0b77261edbfa28c