From 6528571d32a0f95c1f8db340662e117285c9c002 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Mon, 12 Jun 2023 04:15:30 +0000 Subject: [PATCH] adjusted height definition --- comm_alg/krull.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/comm_alg/krull.lean b/comm_alg/krull.lean index 431b8f6..5204b9a 100644 --- a/comm_alg/krull.lean +++ b/comm_alg/krull.lean @@ -20,7 +20,7 @@ namespace Ideal variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J ≤ I} - 1 +noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I