From a62a8bfe4d73b3c5bfa77168fe6f8b13f6b55f46 Mon Sep 17 00:00:00 2001
From: Andre <espietandre@gmail.com>
Date: Wed, 14 Jun 2023 16:37:08 -0400
Subject: [PATCH] removed two imports

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

diff --git a/CommAlg/monalisa.lean b/CommAlg/monalisa.lean
index 43cb907..68579da 100644
--- a/CommAlg/monalisa.lean
+++ b/CommAlg/monalisa.lean
@@ -4,8 +4,6 @@ import Mathlib.Algebra.Module.GradedModule
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Artinian
 import Mathlib.Order.Height
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
-import Mathlib.RingTheory.FiniteType
 
 noncomputable def length ( A : Type _) (M : Type _)
  [CommRing A] [AddCommGroup M] [Module A M] :=  Set.chainHeight {M' : Submodule A M | M' < ⊤}