Skip to content

Import each complete project through its generated root #559

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vilin97 merged 1 commit into from
Oct 1, 2026
Merged

Import each complete project through its generated root #559

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10,254 changes: 255 additions & 9,999 deletions LeanPool.lean
View file
Open in desktop

Large diffs are not rendered by default.

15 changes: 15 additions & 0 deletions LeanPool/ABCExceptions/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.ABCExceptions
public import LeanPool.ABCExceptions.ForMathlib
public import LeanPool.ABCExceptions.ForMathlib.Misc
public import LeanPool.ABCExceptions.ForMathlib.RingTheory
public import LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical
public import LeanPool.ABCExceptions.Section2
public import LeanPool.ABCExceptions.Section4
73 changes: 73 additions & 0 deletions LeanPool/ACMax/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.ACMax
public import LeanPool.ACMax.AHL.AHLAmGm
public import LeanPool.ACMax.AHL.AHLMarginals
public import LeanPool.ACMax.AHL.AHLStationary
public import LeanPool.ACMax.AHL.NBWalk
public import LeanPool.ACMax.AHL.NBWalkCount
public import LeanPool.ACMax.AHL.NBWeighted
public import LeanPool.ACMax.Band.AssemblyAllRange
public import LeanPool.ACMax.Band.CertAllRange
public import LeanPool.ACMax.Band.CertUniform
public import LeanPool.ACMax.Band.Final
public import LeanPool.ACMax.Band.KillSharp
public import LeanPool.ACMax.Band.Rows
public import LeanPool.ACMax.Band.Subset
public import LeanPool.ACMax.Band.Sum
public import LeanPool.ACMax.Counting.Cherry
public import LeanPool.ACMax.Counting.CherryMShape
public import LeanPool.ACMax.Counting.CompactCell
public import LeanPool.ACMax.Counting.CompactLedgers
public import LeanPool.ACMax.Counting.DecoratedC4
public import LeanPool.ACMax.Counting.DoubleStar
public import LeanPool.ACMax.Counting.FarPair
public import LeanPool.ACMax.Counting.HeavyClass
public import LeanPool.ACMax.Counting.HubCross
public import LeanPool.ACMax.Counting.Incidence
public import LeanPool.ACMax.Counting.LargeN
public import LeanPool.ACMax.Counting.MEdgeSparse
public import LeanPool.ACMax.Counting.MoatSharp
public import LeanPool.ACMax.Counting.Moats
public import LeanPool.ACMax.Counting.PoorCorner
public import LeanPool.ACMax.Counting.Quotient
public import LeanPool.ACMax.Counting.ResidualInterface
public import LeanPool.ACMax.Counting.SigmaCloud
public import LeanPool.ACMax.Counting.SmallDegreeThreeCore
public import LeanPool.ACMax.Counting.SparseCore
public import LeanPool.ACMax.Counting.SqrtGirth
public import LeanPool.ACMax.Counting.StarForcing
public import LeanPool.ACMax.Counting.StarMoatSharp
public import LeanPool.ACMax.Counting.StarNeighbors
public import LeanPool.ACMax.Counting.StarvedCensus
public import LeanPool.ACMax.Counting.TripleCensus
public import LeanPool.ACMax.Counting.V9Discharge
public import LeanPool.ACMax.Counting.V9DischargeSharp
public import LeanPool.ACMax.Counting.Windows
public import LeanPool.ACMax.Counting.XBoundAssembly
public import LeanPool.ACMax.Cuts.Disconnected
public import LeanPool.ACMax.Cuts.GoodC4
public import LeanPool.ACMax.Cuts.GoodK23
public import LeanPool.ACMax.Cuts.GoodTriangle
public import LeanPool.ACMax.Cuts.Ind2K2
public import LeanPool.ACMax.Cuts.LowDegreeVertex
public import LeanPool.ACMax.Cuts.SignedCut
public import LeanPool.ACMax.Cuts.TriangleFree2K2
public import LeanPool.ACMax.Cuts.TwoCut
public import LeanPool.ACMax.Cuts.WeightedCut
public import LeanPool.ACMax.InternalEdgesEven
public import LeanPool.ACMax.Reduction.GapReduction
public import LeanPool.ACMax.Reduction.Reduction
public import LeanPool.ACMax.Reduction.Residual
public import LeanPool.ACMax.Spectral.AlgConn
public import LeanPool.ACMax.Spectral.AlgConnK2
public import LeanPool.ACMax.Spectral.RayleighLower
public import LeanPool.ACMax.Spectral.RayleighUpper
public import LeanPool.ACMax.Spectral.TestVector
public import LeanPool.ACMax.UpperBound
54 changes: 54 additions & 0 deletions LeanPool/AFormalizationOfBorelDeterminacyInLean/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.AFormalizationOfBorelDeterminacyInLean
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Choquet
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.General
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Meager
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.RegularOpen
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.FinLists
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.General
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.InfLists
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.InvLimitNat
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.Meta
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.MiscCat
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.BuildStrategies
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.GaleStewart
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Games
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Player
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Strategies
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Undetermined
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BorelDeterminacy
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BuildLevelwise
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Covering
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringClosedGame
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringLim
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Lift
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.PreLift
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Strat
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.WinAsap
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.Lift
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.PreLift
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.Strat
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.TreeLift
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.QualityAliases
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.BodyFunctor
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.LenTreeHom
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.PointedTrees
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.RestrictTree
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeBody
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeExtensions
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeLim
public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.Trees
11 changes: 11 additions & 0 deletions LeanPool/AgreeToDisagree/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.AgreeToDisagree
public import LeanPool.AgreeToDisagree.AgreeToDisagree
public import LeanPool.AgreeToDisagree.AgreeToDisagreeBeliefs
12 changes: 12 additions & 0 deletions LeanPool/AharoniKorman/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.AharoniKorman
public import LeanPool.AharoniKorman.Counterexample
public import LeanPool.AharoniKorman.ForMathlib
public import LeanPool.AharoniKorman.ForMathlib.Misc
58 changes: 58 additions & 0 deletions LeanPool/AndersonConjecture/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.AndersonConjecture
public import LeanPool.AndersonConjecture.AdicKerEval
public import LeanPool.AndersonConjecture.AdicLocal
public import LeanPool.AndersonConjecture.AdicNoetherian
public import LeanPool.AndersonConjecture.Basic
public import LeanPool.AndersonConjecture.CompleteDomain
public import LeanPool.AndersonConjecture.CompleteDomain.CompleteDomain
public import LeanPool.AndersonConjecture.CompleteDomain.Domain
public import LeanPool.AndersonConjecture.CompleteDomain.LocalRing
public import LeanPool.AndersonConjecture.Jensen
public import LeanPool.AndersonConjecture.Jensen.Adjoin
public import LeanPool.AndersonConjecture.Jensen.Adjoin.Adjoin
public import LeanPool.AndersonConjecture.Jensen.Adjoin.FromPrime
public import LeanPool.AndersonConjecture.Jensen.Adjoin.Transcendental
public import LeanPool.AndersonConjecture.Jensen.Application
public import LeanPool.AndersonConjecture.Jensen.Avoidance
public import LeanPool.AndersonConjecture.Jensen.CloseUp
public import LeanPool.AndersonConjecture.Jensen.CloseUp.AvoidanceStep
public import LeanPool.AndersonConjecture.Jensen.CloseUp.Base
public import LeanPool.AndersonConjecture.Jensen.CloseUp.CloseUp
public import LeanPool.AndersonConjecture.Jensen.CloseUp.CoprimeSplit
public import LeanPool.AndersonConjecture.Jensen.CloseUp.Factor
public import LeanPool.AndersonConjecture.Jensen.CloseUp.FactorDivisibility
public import LeanPool.AndersonConjecture.Jensen.CloseUp.GcdComplexity
public import LeanPool.AndersonConjecture.Jensen.CloseUp.IntersectionHelpers
public import LeanPool.AndersonConjecture.Jensen.CloseUp.IntersectionStep
public import LeanPool.AndersonConjecture.Jensen.CloseUp.NoCommonFactor
public import LeanPool.AndersonConjecture.Jensen.CloseUp.TwoGen
public import LeanPool.AndersonConjecture.Jensen.CombinedStep
public import LeanPool.AndersonConjecture.Jensen.Construction
public import LeanPool.AndersonConjecture.Jensen.Construction.ChainHelpers
public import LeanPool.AndersonConjecture.Jensen.Construction.Construction
public import LeanPool.AndersonConjecture.Jensen.Construction.HeitmannProp
public import LeanPool.AndersonConjecture.Jensen.Construction.Transfinite
public import LeanPool.AndersonConjecture.Jensen.Defs
public import LeanPool.AndersonConjecture.Jensen.Jensen
public import LeanPool.AndersonConjecture.Jensen.KrullDomain
public import LeanPool.AndersonConjecture.Jensen.KrullDomain.AdjoinLocSet
public import LeanPool.AndersonConjecture.Jensen.KrullDomain.HeightBound
public import LeanPool.AndersonConjecture.Jensen.KrullDomain.KrullDomain
public import LeanPool.AndersonConjecture.Jensen.KrullDomain.LocUFD
public import LeanPool.AndersonConjecture.Jensen.KrullDomain.Nagata
public import LeanPool.AndersonConjecture.Jensen.KrullDomain.Prime
public import LeanPool.AndersonConjecture.Jensen.KrullDomain.UFDConstruction
public import LeanPool.AndersonConjecture.Jensen.NSubring
public import LeanPool.AndersonConjecture.Jensen.TransfiniteUnion
public import LeanPool.AndersonConjecture.Main
public import LeanPool.AndersonConjecture.QuasiCompleteRing
public import LeanPool.AndersonConjecture.QuasiCompleteRing.Complete
public import LeanPool.AndersonConjecture.QuasiCompleteRing.QuasiCompleteRing
12 changes: 12 additions & 0 deletions LeanPool/Apportionment/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.Apportionment
public import LeanPool.Apportionment.Basic
public import LeanPool.Apportionment.PlausibleInstances
public import LeanPool.Apportionment.Utils
38 changes: 38 additions & 0 deletions LeanPool/ArchonFirstProofResults/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.ArchonFirstProofResults
public import LeanPool.ArchonFirstProofResults.FirstProof4
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.BoxPlusRealRoots
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Continuity
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Defs
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Density
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.HarmonicBound
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.InvPhiN
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Obreschkoff
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.ObreschkoffTransport
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.PhiN
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.RPoly
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.RealRoots
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Residue
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.RootContinuity
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.SignSquarefree
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Transport
public import LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.TransportDecomp
public import LeanPool.ArchonFirstProofResults.FirstProof4.Problem4
public import LeanPool.ArchonFirstProofResults.FirstProof6
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.BarrierPotential
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.ColoringFramework
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.DynamicColoring
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.LaplacianBasics
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.LoewnerPullback
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.OneSidedBarrier
public import LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.ResolventBound
public import LeanPool.ArchonFirstProofResults.FirstProof6.Problem6
21 changes: 21 additions & 0 deletions LeanPool/ArtinWedderburn/Imports.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
/-
Copyright (c) 2026 Lean Pool contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lean Pool contributors
-/
module -- shake: keep-all --deprecated_module: ignore

-- Generated project imports; run `lake exe mk_all`.
public import LeanPool.ArtinWedderburn
public import LeanPool.ArtinWedderburn.ArtinWedderburnTheorem
public import LeanPool.ArtinWedderburn.Auxiliary
public import LeanPool.ArtinWedderburn.CornerCornerLemma
public import LeanPool.ArtinWedderburn.CornerRing
public import LeanPool.ArtinWedderburn.IdealProd
public import LeanPool.ArtinWedderburn.Idempotents
public import LeanPool.ArtinWedderburn.MatrixUnits
public import LeanPool.ArtinWedderburn.MinIdeals
public import LeanPool.ArtinWedderburn.NiceIdeals
public import LeanPool.ArtinWedderburn.NonUnitalToUnital
public import LeanPool.ArtinWedderburn.PrimeRing
public import LeanPool.ArtinWedderburn.SetProd
Loading
Loading