min imports

AntoineChambert-Loir · Oct 19, 2024 · 4d2473a · 4d2473a
1 parent 4f247e1
commit 4d2473a
Show file tree

Hide file tree

Showing 17 changed files with 107 additions and 126 deletions.
diff --git a/DividedPowers/DPAlgebra/BaseChange.lean b/DividedPowers/DPAlgebra/BaseChange.lean
@@ -1,11 +1,5 @@
---import DividedPowers.DPAlgebra.Init
 import DividedPowers.DPAlgebra.Exponential
 import DividedPowers.DPAlgebra.Graded.Basic
-import DividedPowers.ForMathlib.RingTheory.TensorProduct.MvPolynomial
-import DividedPowers.PolynomialMap.Homogeneous
---import DividedPowers.DPAlgebra.Misc
-import Mathlib.Algebra.Algebra.Operations
-import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.RingTheory.TensorProduct.Basic
 
 -- import DividedPowers.ForMathlib.RingTheory.TensorProduct

diff --git a/DividedPowers/DPAlgebra/Envelope.lean b/DividedPowers/DPAlgebra/Envelope.lean
@@ -1,4 +1,5 @@
 import DividedPowers.DPAlgebra.Compatible
+import Mathlib.Data.Rel
 
 universe u v w
 
@@ -357,6 +358,7 @@ lemma isCompatibleWith [Nontrivial B] [DecidableEq B]
     true_and]
     sorry -/
 
+
 #exit
 
 -- End of case 1
@@ -589,5 +591,3 @@ theorem dpEnvelope_IsDPEnvelope [DecidableEq B] [∀ x, Decidable (x ∈  (dpIde
   simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
     MonoidHom.coe_coe]
   rw [← hφ_unique β hβ]
-
-#min_imports
diff --git a/DividedPowers/DPAlgebra/Exponential.lean b/DividedPowers/DPAlgebra/Exponential.lean
@@ -136,3 +136,6 @@ theorem dividedPowerAlgebra_exponentialModule_equiv_symm_apply
       = coeff S n (β m) := by
   unfold dividedPowerAlgebra_exponentialModule_equiv
   simp only [Equiv.coe_fn_symm_mk, lift'AlgHom_apply_dp]
+
+
+#min_imports
diff --git a/DividedPowers/DPAlgebra/Graded/Basic.lean b/DividedPowers/DPAlgebra/Graded/Basic.lean
@@ -1,5 +1,7 @@
 import DividedPowers.DPAlgebra.Init
 import DividedPowers.ForMathlib.GradedRingQuot
+import Mathlib.Algebra.MvPolynomial.CommRing
+
 
 noncomputable section
 

diff --git a/DividedPowers/DPAlgebra/Init.lean b/DividedPowers/DPAlgebra/Init.lean
@@ -5,11 +5,6 @@
 import DividedPowers.Basic
 import DividedPowers.DPAlgebra.Misc
 
-import Mathlib.Algebra.RingQuot
-import Mathlib.Algebra.Algebra.Operations
-import Mathlib.Data.Rel
-import Mathlib.RingTheory.Ideal.Quotient
-
 noncomputable section
 
 open Finset MvPolynomial Ideal.Quotient
@@ -544,5 +539,3 @@ end Functoriality
 end DividedPowerAlgebra
 
 end
-
---#lint
diff --git a/DividedPowers/DPAlgebra/Misc.lean b/DividedPowers/DPAlgebra/Misc.lean
@@ -2,13 +2,11 @@
 ! This file was ported from Lean 3 source module divided_powers.dp_algebra.misc
 -/
 
-import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
+import Mathlib.Algebra.MvPolynomial.Supported
 import Mathlib.Algebra.RingQuot
 import Mathlib.Algebra.TrivSqZeroExt
-import Mathlib.Algebra.Algebra.Operations
-import Mathlib.Algebra.MvPolynomial.Supported
-import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.RingTheory.Ideal.Maps
+import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 
 noncomputable section
 

diff --git a/DividedPowers/DPAlgebra/PolynomialMap.lean b/DividedPowers/DPAlgebra/PolynomialMap.lean
@@ -1,6 +1,5 @@
-import DividedPowers.PolynomialMap.Homogeneous
-import DividedPowers.DPAlgebra.Graded.Basic
 import DividedPowers.DPAlgebra.BaseChange
+import DividedPowers.PolynomialMap.Homogeneous
 
 /-
 
@@ -83,7 +82,6 @@ theorem gamma_mem_grade (n : ℕ) (S : Type*) [CommRing S] [Algebra R S] (m : S
     simp only [LinearMap.mem_range]
     -- we need the graded structure on the base change of a graded algebra
     rw [← hx', ← hy']
-
     sorry
 
 /- to do this, it seems that we have to understand polynomial maps

diff --git a/DividedPowers/DPAlgebra/RobyLemma9.lean b/DividedPowers/DPAlgebra/RobyLemma9.lean
@@ -1,7 +1,5 @@
-import Mathlib.RingTheory.TensorProduct.Basic
-import Mathlib.LinearAlgebra.TensorProduct.Tower
 import Mathlib.RingTheory.Ideal.QuotientOperations
-import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.RingTheory.TensorProduct.Basic
 
 open scoped TensorProduct