bump

leanprover-community · Nov 30, 2023 · 706af7f · 706af7f
1 parent a3c43d2
commit 706af7f
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean
@@ -78,7 +78,7 @@ lemma primesOver_finite [Ring.DimensionLEOne R] [IsDedekindDomain S] [NoZeroSMul
 
 lemma primesOver_nonempty [IsDomain S] [NoZeroSMulDivisors R S] (hRS : Algebra.IsIntegral R S)
     (p : Ideal R) [p.IsPrime] : (primesOver S p).Nonempty := by
-  have := Ideal.bot_prime (R := S)
+  have := Ideal.bot_prime (α := S)
   obtain ⟨Q, _, hQ⟩ := Ideal.exists_ideal_over_prime_of_isIntegral hRS p ⊥
     (by rw [Ideal.comap_bot_of_injective _
       (NoZeroSMulDivisors.algebraMap_injective R S)]; exact bot_le)

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "6490dc26c9b9ae6687a37af39260ee60ba009035",
+   "rev": "153b6b05d3c8191a7ea093279d19ee4d601b0962",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.3.0
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.3.0-rc2
		leanprover/lean4:v4.3.0