Split project cards and remove the shared import list

LeanPool.lean

@@ -1,294 +1,4 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
-public import LeanPool.ABCExceptions.Imports
-public import LeanPool.ACMax.Imports
-public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Imports
-public import LeanPool.AgreeToDisagree.Imports
-public import LeanPool.AharoniKorman.Imports
-public import LeanPool.AndersonConjecture.Imports
-public import LeanPool.AnomalousDiffusion.Imports
-public import LeanPool.Apportionment.Imports
-public import LeanPool.ArchonFirstProofResults.Imports
-public import LeanPool.ArtinWedderburn.Imports
-public import LeanPool.AsymptoticTrianglePacking.Imports
-public import LeanPool.BKARForestFormula.Imports
-public import LeanPool.BannaiBannaiStanton.Imports
-public import LeanPool.Basic.Imports
-public import LeanPool.BeckFialaMatrix.Imports
-public import LeanPool.Besicovitch.Imports
-public import LeanPool.BeyondBethe.Imports
-public import LeanPool.BicausalOT.Imports
-public import LeanPool.Biswal.Imports
-public import LeanPool.BlockSpectralSensitivity.Imports
-public import LeanPool.BollobasNikiforov.Imports
-public import LeanPool.BooleanIsoperimetry.Imports
-public import LeanPool.BooleanMultiplication.Imports
-public import LeanPool.BrauerGroupNew.Imports
-public import LeanPool.BrillNoetherGraphs.Imports
-public import LeanPool.BrooksSubcubic.Imports
-public import LeanPool.Brouwer.Imports
-public import LeanPool.BruhatTits.Imports
-public import LeanPool.Burkholder.Imports
-public import LeanPool.CIVAxisymmetric.Imports
-public import LeanPool.CaffarelliKohnNirenberg.Imports
-public import LeanPool.CarlsonFunctions.Imports
-public import LeanPool.CencovPetz.Imports
-public import LeanPool.CenteredMaximal.Imports
-public import LeanPool.Champernowne.Imports
-public import LeanPool.ChannelCapacity.Imports
-public import LeanPool.ChipFiring.Imports
-public import LeanPool.Chudnovsky.Imports
-public import LeanPool.Chvatal.Imports
-public import LeanPool.CircuitComplexity.Imports
-public import LeanPool.Circuitlib.Imports
-public import LeanPool.ClassificationOfSurfaces.Imports
-public import LeanPool.Clawristotle.Imports
-public import LeanPool.CommonNeighbourConjecture.Imports
-public import LeanPool.CompactSpectral.Imports
-public import LeanPool.CompactnessAndDegeneracy.Imports
-public import LeanPool.CompositionAlgebras.Imports
-public import LeanPool.Computability.Imports
-public import LeanPool.ComputableReal.Imports
-public import LeanPool.ConcentrationInequalities.Imports
-public import LeanPool.ConnesKreimer.Imports
-public import LeanPool.ConnesRigidity.Imports
-public import LeanPool.ConwayRefinement.Imports
-public import LeanPool.ConwaySoifer.Imports
-public import LeanPool.CramerWold.Imports
-public import LeanPool.CriticalPortraits.Imports
-public import LeanPool.CutAndProject.Imports
-public import LeanPool.DavisKahan.Imports
-public import LeanPool.DeadEnds.Imports
-public import LeanPool.DemazureOperatorsLean.Imports
-public import LeanPool.DemazureProduct.Imports
-public import LeanPool.DensityHalesJewett.Imports
-public import LeanPool.Desargues.Imports
-public import LeanPool.Dilatations.Imports
-public import LeanPool.DirectedTopologyLean4.Imports
-public import LeanPool.DistanceGeometry.Imports
-public import LeanPool.DomainTheory.Imports
-public import LeanPool.DrossFractionalTriangleDecomposition.Imports
-public import LeanPool.Duality.Imports
-public import LeanPool.EcTateLean.Imports
-public import LeanPool.Egrs75.Imports
-public import LeanPool.EhrhartVolumeInequality.Imports
-public import LeanPool.EilenbergZilber.Imports
-public import LeanPool.EllipticPDE.Imports
-public import LeanPool.Erdos1196.Imports
-public import LeanPool.Erdos132ConvexK3.Imports
-public import LeanPool.Erdos132N14.Imports
-public import LeanPool.Erdos132ThreeChain.Imports
-public import LeanPool.Erdos137.Imports
-public import LeanPool.Erdos346.Imports
-public import LeanPool.Erdos367.Imports
-public import LeanPool.Erdos403.Imports
-public import LeanPool.Erdos548.Imports
-public import LeanPool.Erdos81PaperIContrib.Imports
-public import LeanPool.Erdos81PaperIIContrib.Imports
-public import LeanPool.Erdos81PaperIIIContrib.Imports
-public import LeanPool.Erdos865.Imports
-public import LeanPool.Erdos97ConvexOctagon.Imports
-public import LeanPool.ErdosGinzburgZiv.Imports
-public import LeanPool.ErdosMoser.Imports
-public import LeanPool.ErdosTuzaValtr.Imports
-public import LeanPool.EscauriazaSereginSverak.Imports
-public import LeanPool.EuclideanJordan.Imports
-public import LeanPool.EvenGraphCycles.Imports
-public import LeanPool.EventStructures.Imports
-public import LeanPool.ExpChaotic.Imports
-public import LeanPool.FactorizationSystems.Imports
-public import LeanPool.Feige.Imports
-public import LeanPool.FelConjecture.Imports
-public import LeanPool.Fineqs.Imports
-public import LeanPool.FiniteGraphFundamentalGroup.Imports
-public import LeanPool.FiveEighthsTheorem.Imports
-public import LeanPool.Flean.Imports
-public import LeanPool.FltRegular.Imports
-public import LeanPool.FoZfc.Imports
-public import LeanPool.FormalLearningTheory.Imports
-public import LeanPool.FormalizationOfBoundedArithmetic.Imports
-public import LeanPool.FormalizingGMT.Imports
-public import LeanPool.FourAP.Imports
-public import LeanPool.FriezePatterns.Imports
-public import LeanPool.FrontierMathOpenHypergraphs.Imports
-public import LeanPool.FullyDynamicMatching.Imports
-public import LeanPool.FundamentalInequality.Imports
-public import LeanPool.GKPCarry.Imports
-public import LeanPool.GapCVP.Imports
-public import LeanPool.GaussianMomentsCounterexamples.Imports
-public import LeanPool.GoemansFlow.Imports
-public import LeanPool.GranvilleMoore.Imports
-public import LeanPool.GraphColouringMatching.Imports
-public import LeanPool.GrothendieckVanishing.Imports
-public import LeanPool.HSDInteriorPointLP.Imports
-public import LeanPool.HadwigerNelsonBounds.Imports
-public import LeanPool.HansonWright.Imports
-public import LeanPool.HardSphereNBC.Imports
-public import LeanPool.HasseMinkowski.Imports
-public import LeanPool.HopfProblem.Imports
-public import LeanPool.Incompleteness.Imports
-public import LeanPool.InfinitaryLogic.Imports
-public import LeanPool.InfiniteConnesRigidity.Imports
-public import LeanPool.InflationTermination.Imports
-public import LeanPool.IsTranscendentalPi.Imports
-public import LeanPool.IsoGraph.Imports
-public import LeanPool.Isoperimetric.Imports
-public import LeanPool.JacobianDiffgeo.Imports
-public import LeanPool.JohnsonLindenstraussLean.Imports
-public import LeanPool.KahnKalai.Imports
-public import LeanPool.KaltonPeck.Imports
-public import LeanPool.KaltonRoberts.Imports
-public import LeanPool.KasamiCyclicAdditive.Imports
-public import LeanPool.Koethe.Imports
-public import LeanPool.Komlos.Imports
-public import LeanPool.KrafftSieve.Imports
-public import LeanPool.KrohnRhodes.Imports
-public import LeanPool.Kuramoto.Imports
-public import LeanPool.Kurosh.Imports
-public import LeanPool.LanguageGeneration.Imports
-public import LeanPool.LatticeTriangle.Imports
-public import LeanPool.Lean4GlCoalgebras.Imports
-public import LeanPool.Lean4Itree.Imports
-public import LeanPool.LeanBooleanfun.Imports
-public import LeanPool.LeanComplexAnalysis.Imports
-public import LeanPool.LeanModelChecking.Imports
-public import LeanPool.LeanModularForms.Imports
-public import LeanPool.LeanPolyABC.Imports
-public import LeanPool.LeanQuantumAlg.Imports
-public import LeanPool.LeanStationaryHarmonicMaps.Imports
-public import LeanPool.LehmerE10.Imports
-public import LeanPool.Lentil.Imports
-public import LeanPool.LiCriterion.Imports
-public import LeanPool.ListEdgeColoringComplete.Imports
-public import LeanPool.LocalComplexGeometry.Imports
-public import LeanPool.LongGapsBetweenPrimes.Imports
-public import LeanPool.LowDimSolvClassification.Imports
-public import LeanPool.LowWeightPauliDynamics.Imports
-public import LeanPool.MRiscX.Imports
-public import LeanPool.Malliavin.Imports
-public import LeanPool.MarkoffModP.Imports
-public import LeanPool.MarkovProcess.Imports
-public import LeanPool.MarshallHall.Imports
-public import LeanPool.MassFormula.Imports
-public import LeanPool.MatchingLogic.Imports
-public import LeanPool.MaxFlowMinCut.Imports
-public import LeanPool.MetricCodes.Imports
-public import LeanPool.MicrowaveNetworks.Imports
-public import LeanPool.MinModulusUniqueMultisetSum.Imports
-public import LeanPool.MinimumDegreeMatching.Imports
-public import LeanPool.MisereGames.Imports
-public import LeanPool.Monlib4.Imports
-public import LeanPool.Monsky.Imports
-public import LeanPool.MooreBound.Imports
-public import LeanPool.MoserLatticeColorings.Imports
-public import LeanPool.MovingSofa.Imports
-public import LeanPool.MulticolorTriangleRamsey.Imports
-public import LeanPool.NFWeakPartition.Imports
-public import LeanPool.NagataFactoriality.Imports
-public import LeanPool.NandakumarRamanaRao.Imports
-public import LeanPool.NashEmbedding.Imports
-public import LeanPool.NashWilliams.Imports
-public import LeanPool.NaslundCounterexample.Imports
-public import LeanPool.NavierStokesAndEuler.Imports
-public import LeanPool.NemytskiiLebesgue.Imports
-public import LeanPool.Neukirch.Imports
-public import LeanPool.Nikodym.Imports
-public import LeanPool.Nivat.Imports
-public import LeanPool.NonSoficGroup.Imports
-public import LeanPool.OSforGFF.Imports
-public import LeanPool.OddPrimeValuationDistribution.Imports
-public import LeanPool.Odlyzko.Imports
-public import LeanPool.OneManifold.Imports
-public import LeanPool.OperatorTheory.Imports
-public import LeanPool.OrderClosures.Imports
-public import LeanPool.OrderPQ.Imports
-public import LeanPool.PCFTheory.Imports
-public import LeanPool.PDL.Imports
-public import LeanPool.PFR.Imports
-public import LeanPool.PLAcceleratedNesterovLean.Imports
-public import LeanPool.PaperIVCliqueTree.Imports
-public import LeanPool.ParallelPostulate.Imports
-public import LeanPool.ParameterFreeGradient.Imports
-public import LeanPool.PartialCombinatoryAlgebras.Imports
-public import LeanPool.PartialRegularity.Imports
-public import LeanPool.PebblingLean.Imports
-public import LeanPool.PentagonalNumberTheorem.Imports
-public import LeanPool.PentagonalNumberTheoremAnalytic.Imports
-public import LeanPool.PermanentFormulaLowerBound.Imports
-public import LeanPool.PhaseRetrieval.Imports
-public import LeanPool.PoincareThreeBody.Imports
-public import LeanPool.PointwiseBirkhoff.Imports
-public import LeanPool.PolyaEnumerationTheorem.Imports
-public import LeanPool.Polylean.Imports
-public import LeanPool.PolylogIntegrals.Imports
-public import LeanPool.PolynomialMethodRestrictedSums.Imports
-public import LeanPool.Polytopes.Imports
-public import LeanPool.Puiseux.Imports
-public import LeanPool.PumpingCfg.Imports
-public import LeanPool.PythagoreanPolynomialParametrization.Imports
-public import LeanPool.QECCertificates.Imports
-public import LeanPool.QuadraticCarleson.Imports
-public import LeanPool.QuadraticIterates.Imports
-public import LeanPool.QuantumParallelRepetition.Imports
-public import LeanPool.QuantumQuery.Imports
-public import LeanPool.QuasiBorelSpaces.Imports
-public import LeanPool.Rado.Imports
-public import LeanPool.RamanujanNagell.Imports
-public import LeanPool.RamanujanTauMissesPrimes.Imports
-public import LeanPool.RearrangementNumber.Imports
-public import LeanPool.Redhill.Imports
-public import LeanPool.RegtsSevenster.Imports
-public import LeanPool.RellichKondrachov.Imports
-public import LeanPool.RiemannMappingTheorem.Imports
-public import LeanPool.RiemannRochFunctionFields.Imports
-public import LeanPool.RlTheoryInLean.Imports
-public import LeanPool.RootSystem.Imports
-public import LeanPool.RungeKuttaOrderConditions.Imports
-public import LeanPool.Rupert.Imports
-public import LeanPool.SNumbers.Imports
-public import LeanPool.Sabidussi.Imports
-public import LeanPool.SalemTheorem.Imports
-public import LeanPool.SardMoreira.Imports
-public import LeanPool.Schoenflies.Imports
-public import LeanPool.ScottishBook155.Imports
-public import LeanPool.SelbergSieve4.Imports
-public import LeanPool.SemicircleCheck.Imports
-public import LeanPool.SemicircleLaw.Imports
-public import LeanPool.Sendov.Imports
-public import LeanPool.Sensitivity.Imports
-public import LeanPool.SetTheory.Imports
-public import LeanPool.SeveralComplexVariables.Imports
-public import LeanPool.Shannon1948Formalization.Imports
-public import LeanPool.SingularModuli.Imports
-public import LeanPool.SmallUndecidableGroups.Imports
-public import LeanPool.SpectralPositivity.Imports
-public import LeanPool.SpectralTheory.Imports
-public import LeanPool.SpherePacking.Imports
-public import LeanPool.Stafford38.Imports
-public import LeanPool.StallingsFolding.Imports
-public import LeanPool.SteinhausThreeGap.Imports
-public import LeanPool.StructuralGraphClasses.Imports
-public import LeanPool.SumDifferenceExponent.Imports
-public import LeanPool.SumsThreeSquares.Imports
-public import LeanPool.Sundogcert.Imports
-public import LeanPool.Superorthogonality.Imports
-public import LeanPool.SyntheticEuclid4.Imports
-public import LeanPool.ThreeGap.Imports
-public import LeanPool.Turan3.Imports
-public import LeanPool.TuttePath.Imports
-public import LeanPool.TwoColoringOneRound.Imports
-public import LeanPool.UlmsTheorem.Imports
-public import LeanPool.UnconditionalSchauderBasis.Imports
-public import LeanPool.VirasoroProject.Imports
-public import LeanPool.ViscositySolutionTheory.Imports
-public import LeanPool.Vizing.Imports
-public import LeanPool.Vlasov.Imports
-public import LeanPool.Wallace.Imports
-public import LeanPool.WhiteheadTheorem.Imports
-public import LeanPool.ZFLean.Imports
-public import LeanPool.Zeta32.Imports
-public import LeanPool.Zeta3Irrational.Imports
-public import LeanPool.Zeta5Irrational.Imports
-public import LeanPool.ZetaH123.Imports
-public import LeanPool.ZetaZeros.Imports
-public import LeanPool.ZhangYeungInequality.Imports
+-- Lake builds every LeanPool module directly. Import a project's
+-- Imports module to use its complete public API.