-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathDividedPowers.lean
53 lines (53 loc) · 3.14 KB
/
DividedPowers.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
--import DividedPowers.Basic -- In PR #15657
import DividedPowers.BasicLemmas
import DividedPowers.DPAlgebra.BaseChange -- It uses sorry
import DividedPowers.DPAlgebra.Compatible -- It uses sorry (depended on AlgebraComp)
import DividedPowers.DPAlgebra.Dpow -- It uses sorry (depended on RobyLemma5)
import DividedPowers.DPAlgebra.Envelope -- It uses sorry (depended on AlgebraComp)
import DividedPowers.DPAlgebra.Exponential
import DividedPowers.DPAlgebra.Graded.Basic
import DividedPowers.DPAlgebra.Graded.GradeOne
import DividedPowers.DPAlgebra.Graded.GradeZero
import DividedPowers.DPAlgebra.Init
import DividedPowers.DPAlgebra.Misc
import DividedPowers.DPAlgebra.PolynomialMap -- It uses sorry
import DividedPowers.DPAlgebra.RobyLemma9
import DividedPowers.DPMorphism --In PR #22318
import DividedPowers.ExponentialModule.Basic
import DividedPowers.Exponential
import DividedPowers.ForMathlib.AlgebraLemmas -- In PR #22237, #22239 and #22240.
--import DividedPowers.ForMathlib.Bell -- -- In PR #15644
import DividedPowers.ForMathlib.DirectLimit
import DividedPowers.ForMathlib.GradedBaseChange
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.RingTheory.AugmentationIdeal -- uses sorry.
import DividedPowers.ForMathlib.RingTheory.MvPowerSeries.Evaluation -- In PR 15019
--import DividedPowers.ForMathlib.RingTheory.MvPowerSeries.LinearTopology -- In PR #15007
--import DividedPowers.ForMathlib.RingTheory.MvPowerSeries.Order -- In PR #14983
--import DividedPowers.ForMathlib.RingTheory.MvPowerSeries.PiTopology -- In PR #14866 and PR #14989
import DividedPowers.ForMathlib.RingTheory.MvPowerSeries.StronglySummable.Basic -- it uses sorry
import DividedPowers.ForMathlib.RingTheory.MvPowerSeries.StronglySummable.Topology
--import DividedPowers.ForMathlib.MvPowerSeries.Sandbox -- Test file, do not import here.
import DividedPowers.ForMathlib.RingTheory.MvPowerSeries.Substitution
--import DividedPowers.ForMathlib.MvPowerSeries.Trunc -- In PR 20958
--import DividedPowers.ForMathlib.RingTheory.PowerSeries.Topology -- In PR #14866
import DividedPowers.ForMathlib.RingTheory.SubmoduleMem
import DividedPowers.ForMathlib.RingTheory.PowerSeries.Evaluation
import DividedPowers.ForMathlib.RingTheory.TensorProduct.LinearEquiv
import DividedPowers.ForMathlib.RingTheory.TensorProduct.MonoidAlgebra
import DividedPowers.ForMathlib.RingTheory.TensorProduct.MvPolynomial
import DividedPowers.ForMathlib.RingTheory.TensorProduct.Polynomial
import DividedPowers.ForMathlib.Topology.Algebra.LinearTopology
--import DividedPowers.ForMathlib.Topology.Algebra.TopologicallyNilpotent -- In PR #20971
import DividedPowers.IdealAdd
--import DividedPowers.IdealAdd2 --NOTE: we cannot import this because it
-- duplicates lemmas from IdealAdd. We should pick a version.
import DividedPowers.Padic
import DividedPowers.PolynomialMap.Basic
import DividedPowers.PolynomialMap.Coeff
import DividedPowers.PolynomialMap.Homogeneous -- It has a sorry
import DividedPowers.RatAlgebra -- In PR #22322
import DividedPowers.SubDPIdeal