From 0773a97fb544e404b0f7dfcc2707d08f6b79104e Mon Sep 17 00:00:00 2001 From: Andre Date: Wed, 14 Jun 2023 16:28:25 -0400 Subject: [PATCH] reduced imports poly_type --- CommAlg/poly_type.lean | 20 +------------------- 1 file changed, 1 insertion(+), 19 deletions(-) diff --git a/CommAlg/poly_type.lean b/CommAlg/poly_type.lean index ab3b4c1..52fa754 100644 --- a/CommAlg/poly_type.lean +++ b/CommAlg/poly_type.lean @@ -1,24 +1,6 @@ -import Mathlib -import Mathlib.Algebra.MonoidAlgebra.Basic -import Mathlib.Data.Finset.Sort import Mathlib.Order.Height -import Mathlib.Order.KrullDimension -import Mathlib.Order.JordanHolder import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -import Mathlib.Order.Height -import Mathlib.RingTheory.Ideal.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.Algebra.Module.GradedModule -import Mathlib.RingTheory.Noetherian -import Mathlib.RingTheory.Finiteness -import Mathlib.RingTheory.Ideal.Operations + -- Setting for "library_search" set_option maxHeartbeats 0