From 4f2005ca08033bcfd40dc1584e4afafb24752f09 Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Sat, 17 Jun 2023 20:04:04 -0500
Subject: [PATCH] change: Removed one unneeded line

---
 CommAlg/krull.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean
index 9709f7c..59b1517 100644
--- a/CommAlg/krull.lean
+++ b/CommAlg/krull.lean
@@ -386,7 +386,6 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD
   · unfold krullDim
     apply @iSup_le (WithBot ℕ∞) _ _ _ _
     intro I
-    have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance
     by_cases I = ⊥
     · rw [← height_zero_iff_bot] at h
       simp only [WithBot.coe_le_one, ge_iff_le]