From a941cce12f21b0bd94757a669c1d73f5677c60a5 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Tue, 13 Jun 2023 14:26:19 -0700 Subject: [PATCH] changed all rings from Type to Type _ --- CommAlg/krull.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 440ea66..2a87c16 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -25,11 +25,11 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} -noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I +noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl -lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl -lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl +lemma krullDim_def (R : Type _) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl +lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice @@ -39,16 +39,16 @@ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ show J' < J exact lt_of_lt_of_le hJ' I_le_J -lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : +lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) : krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) -lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) : +lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) : krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) -lemma le_krullDim_iff (R : Type) [CommRing R] (n : ℕ) : +lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry -lemma le_krullDim_iff' (R : Type) [CommRing R] (n : ℕ∞) : +lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry @[simp]