From 7b8c0ba127128bfb3bd11221291139e087978e03 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:35:46 -0700 Subject: [PATCH] Made very small changes --- CommAlg/sayantan(dim_eq_zero_iff_field).lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CommAlg/sayantan(dim_eq_zero_iff_field).lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean index 35f197f..fd712f0 100644 --- a/CommAlg/sayantan(dim_eq_zero_iff_field).lean +++ b/CommAlg/sayantan(dim_eq_zero_iff_field).lean @@ -68,7 +68,7 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this rw [←Set.one_le_chainHeight_iff] at this exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) - have zero_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by + have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le rw [iSup_le_iff] at this exact Iff.mp WithBot.coe_le_zero (this P')