From d0a6d8605e8a8b38a7e6cc9ea2312a2641015d8a Mon Sep 17 00:00:00 2001
From: leopoldmayer <leomayer@uw.edu>
Date: Fri, 16 Jun 2023 09:54:07 -0700
Subject: [PATCH] golfed imports

---
 CommAlg/polynomial.lean | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/CommAlg/polynomial.lean b/CommAlg/polynomial.lean
index 8dd886a..e7380b0 100644
--- a/CommAlg/polynomial.lean
+++ b/CommAlg/polynomial.lean
@@ -1,13 +1,3 @@
-import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.RingTheory.FiniteType
-import Mathlib.Order.Height
-import Mathlib.RingTheory.Polynomial.Quotient
-import Mathlib.RingTheory.PrincipalIdealDomain
-import Mathlib.RingTheory.DedekindDomain.Basic
-import Mathlib.RingTheory.Ideal.Quotient
-import Mathlib.RingTheory.Localization.AtPrime
-import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import CommAlg.krull
 
 section ChainLemma
@@ -132,7 +122,6 @@ lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I
       apply hl.2
       exact hb
 
-#check (⊤ : ℕ∞)
 /-
 dim R + 1 ≤ dim R[X]
 -/