From 7173aefe8d9e171bac69d087b87a9276d30ba70b Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Wed, 14 Jun 2023 17:43:16 +0000 Subject: [PATCH] changed type of 1 in dim_le_one_of_dimLEOne --- CommAlg/krull.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 06e6d0d..27c3d7e 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -197,7 +197,8 @@ height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' /-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib applies only to dimension zero rings and domains of dimension 1. -/ -lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by +lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by + show _ → ((_ : WithBot ℕ∞) ≤ (1 : ℕ)) rw [krullDim_le_iff R 1] intro H p apply le_of_not_gt