From a1888c51e6da1b9bc49a00000f2cd2a2a6554319 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Wed, 14 Jun 2023 15:07:21 -0400
Subject: [PATCH] removed imports

---
 CommAlg/monalisa.lean | 22 ----------------------
 1 file changed, 22 deletions(-)

diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean
index e815cb2..717e95a 100644
--- a/CommAlg/monalisa.lean
+++ b/CommAlg/monalisa.lean
@@ -1,31 +1,9 @@
 import Mathlib.Order.KrullDimension
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
-import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.RingTheory.GradedAlgebra.Basic
-import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
 import Mathlib.Algebra.Module.GradedModule
 import Mathlib.RingTheory.Ideal.AssociatedPrime
-import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.Artinian
-import Mathlib.RingTheory.FiniteType
 import Mathlib.Order.Height
-import Mathlib.RingTheory.PrincipalIdealDomain
-import Mathlib.RingTheory.DedekindDomain.Basic
-import Mathlib.RingTheory.Ideal.Quotient
-import Mathlib.RingTheory.Localization.AtPrime
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
-import Mathlib.Algebra.DirectSum.Ring
-import Mathlib.RingTheory.Ideal.LocalRing
---import Mathlib
-import Mathlib.Algebra.MonoidAlgebra.Basic
-import Mathlib.Data.Finset.Sort
-import Mathlib.Order.JordanHolder
-import Mathlib.RingTheory.Ideal.Basic
-import Mathlib.RingTheory.Finiteness
-
-
-
 
 noncomputable def length ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}