update DividedPowers.lean

AntoineChambert-Loir · Sep 18, 2024 · 076544e · 076544e
1 parent 029aced
commit 076544e
Showing 1 changed file with 13 additions and 16 deletions.
diff --git a/DividedPowers.lean b/DividedPowers.lean
@@ -1,42 +1,39 @@
 import DividedPowers.Basic
 import DividedPowers.BasicLemmas
-import DividedPowers.DPAlgebra.BaseChange -- It uses sorry
+--import DividedPowers.DPAlgebra.BaseChange -- TODO: import after updating from PR #15158 -- It uses sorry
 --import DividedPowers.DPAlgebra.Compatible -- TODO: fix (depends on Dpow) -- It uses sorry (depended on AlgebraComp)
 --import DividedPowers.DPAlgebra.Dpow -- It uses sorry (depended on RobyLemma5) --TODO: fix (depends on IdealAdd)
--- import DividedPowers.DPAlgebra.Envelope  -- TODO: fix (depends on Dpow) -- It uses sorry (depended on AlgebraComp)
-import DividedPowers.DPAlgebra.Exponential
+--import DividedPowers.DPAlgebra.Envelope  -- TODO: fix (depends on Dpow) -- It uses sorry (depended on AlgebraComp)
+--import DividedPowers.DPAlgebra.Exponential -- TODO: import after updating from PR #15158
 import DividedPowers.DPAlgebra.Graded.Basic
 import DividedPowers.DPAlgebra.Graded.GradeOne
 import DividedPowers.DPAlgebra.Graded.GradeZero
 import DividedPowers.DPAlgebra.Init
-import DividedPowers.DPAlgebra.Misc -- It uses sorry
-import DividedPowers.DPAlgebra.PolynomialMap -- It uses sorry
+import DividedPowers.DPAlgebra.Misc
+--import DividedPowers.DPAlgebra.PolynomialMap -- TODO: import after updating from PR #15158 -- It uses sorry
 import DividedPowers.DPAlgebra.RobyLemma9
 import DividedPowers.DPMorphism
-import DividedPowers.ExponentialModule.Basic
-import DividedPowers.Exponential
+--import DividedPowers.ExponentialModule.Basic -- TODO: import after updating from PR #15158
+-- import DividedPowers.Exponential -- TODO: import after updating from PR #15158
 --import DividedPowers.ForMathlib.AlgebraComp -- This file has errors, but I think we should not use it
 import DividedPowers.ForMathlib.AlgebraLemmas
 import DividedPowers.ForMathlib.Bell
 -- import DividedPowers.ForMathlib.CombinatoricsLemmas -- this was a previous version, now Bell
 import DividedPowers.ForMathlib.DirectLimit
---import DividedPowers.ForMathlib.GradedAlgebra -- This does not exist
---import DividedPowers.ForMathlib.GradedModuleQuot -- Not ported
+--import DividedPowers.ForMathlib.GradedModuleQuot -- Not ported, do not import here
 import DividedPowers.ForMathlib.GradedRingQuot
 --import DividedPowers.ForMathlib.InfiniteSum.Basic -- In mathlib
 --import DividedPowers.ForMathlib.InfiniteSum.Order -- In mathlib
 import DividedPowers.ForMathlib.Lcoeff
 --import DividedPowers.ForMathlib.MvPowerSeries.Basic
 import DividedPowers.ForMathlib.MvPowerSeries.Evaluation -- In PR 15019
-import DividedPowers.ForMathlib.MvPowerSeries.LinearTopology -- it uses sorry
+import DividedPowers.ForMathlib.MvPowerSeries.LinearTopology
 import DividedPowers.ForMathlib.MvPowerSeries.Order -- -- In PR 14983
---import DividedPowers.ForMathlib.MvPowerSeries.Sandbox
+import DividedPowers.ForMathlib.MvPowerSeries.PiTopology -- In PR 14866 and 14989
 import DividedPowers.ForMathlib.MvPowerSeries.StronglySummable.Basic -- it uses sorry
 import DividedPowers.ForMathlib.MvPowerSeries.StronglySummable.Topology
-import DividedPowers.ForMathlib.MvPowerSeries.Substitutions
-import DividedPowers.ForMathlib.MvPowerSeries.PiTopology -- In PR 14866 and 14989
---import DividedPowers.ForMathlib.MvPowerSeries.Sandbox --TODO: ask if this is needed
-import DividedPowers.ForMathlib.MvPowerSeries.Substitutions -- it uses sorry
+--import DividedPowers.ForMathlib.MvPowerSeries.Sandbox -- Test file, do not import here.
+--import DividedPowers.ForMathlib.MvPowerSeries.Substitution -- TODO: import after updating from PR #15158
 import DividedPowers.ForMathlib.MvPowerSeries.Trunc
 import DividedPowers.ForMathlib.PowerSeries.Topology
 --import DividedPowers.ForMathlib.RingTheory.Ideal
@@ -45,7 +42,7 @@ import DividedPowers.ForMathlib.RingTheory.SubmoduleMem
 import DividedPowers.ForMathlib.RingTheory.TensorProduct.LinearEquiv
 import DividedPowers.ForMathlib.RingTheory.TensorProduct.MvPolynomial
 import DividedPowers.ForMathlib.RingTheory.TensorProduct.Polynomial
-import DividedPowers.ForMathlib.Topology.Algebra.LinearTopology -- It has sorrys
+import DividedPowers.ForMathlib.Topology.Algebra.LinearTopology
 import DividedPowers.IdealAdd
 import DividedPowers.PolynomialMap.Basic
 import DividedPowers.PolynomialMap.Coeff