From 076544e8f991dc0c82511508c6fcfe2c1b430e62 Mon Sep 17 00:00:00 2001 From: mariainesdff Date: Wed, 18 Sep 2024 13:39:36 +0200 Subject: [PATCH] update DividedPowers.lean --- DividedPowers.lean | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/DividedPowers.lean b/DividedPowers.lean index 62f0440..2a90e48 100644 --- 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