Documentation
LeanPool
Search
return to top
source
Imports
Init
LeanPool.ABCExceptions
LeanPool.AFormalizationOfBorelDeterminacyInLean
LeanPool.AgreeToDisagree
LeanPool.AharoniKorman
LeanPool.AndersonConjecture
LeanPool.Apportionment
LeanPool.ArchonFirstProofResults
LeanPool.ArtinWedderburn
LeanPool.Basic
LeanPool.Biswal
LeanPool.BrauerGroupNew
LeanPool.Brouwer
LeanPool.BruhatTits
LeanPool.Burkholder
LeanPool.CencovPetz
LeanPool.CircuitComplexity
LeanPool.Circuitlib
LeanPool.Clawristotle
LeanPool.CompactSpectral
LeanPool.Computability
LeanPool.ComputableReal
LeanPool.ConnesKreimer
LeanPool.CramerWold
LeanPool.CriticalPortraits
LeanPool.DeadEnds
LeanPool.DemazureOperatorsLean
LeanPool.DemazureProduct
LeanPool.Desargues
LeanPool.DirectedTopologyLean4
LeanPool.DomainTheory
LeanPool.Duality
LeanPool.EcTateLean
LeanPool.Egrs75
LeanPool.Erdos1196
LeanPool.Erdos137
LeanPool.Erdos367
LeanPool.Erdos403
LeanPool.ErdosTuzaValtr
LeanPool.EventStructures
LeanPool.FactorizationSystems
LeanPool.FelConjecture
LeanPool.Fineqs
LeanPool.FiveEighthsTheorem
LeanPool.Flean
LeanPool.FoZfc
LeanPool.FormalLearningTheory
LeanPool.FormalizationOfBoundedArithmetic
LeanPool.ForwardEuler
LeanPool.FriezePatterns
LeanPool.FrontierMathOpenHypergraphs
LeanPool.FundamentalInequality
LeanPool.GrothendieckVanishing
LeanPool.HSDInteriorPointLP
LeanPool.Incompleteness
LeanPool.IsTranscendentalPi
LeanPool.Isoperimetric
LeanPool.KaltonRoberts
LeanPool.KrafftSieve
LeanPool.LatticeTriangle
LeanPool.Lean4GlCoalgebras
LeanPool.Lean4Itree
LeanPool.LeanBooleanfun
LeanPool.LeanComplexAnalysis
LeanPool.LeanModelChecking
LeanPool.LeanModularForms
LeanPool.LeanPolyABC
LeanPool.LeanQuantumAlg
LeanPool.Lentil
LeanPool.LowDimSolvClassification
LeanPool.MRiscX
LeanPool.MisereGames
LeanPool.Monlib4
LeanPool.Monsky
LeanPool.Neukirch
LeanPool.OSforGFF
LeanPool.OrderPQ
LeanPool.PCFTheory
LeanPool.PLAcceleratedNesterovLean
LeanPool.PartialCombinatoryAlgebras
LeanPool.PartialRegularity
LeanPool.PebblingLean
LeanPool.PentagonalNumberTheorem
LeanPool.PhaseRetrieval
LeanPool.PointwiseBirkhoff
LeanPool.PolyaEnumerationTheorem
LeanPool.Polylean
LeanPool.PolynomialMethodRestrictedSums
LeanPool.Polytopes
LeanPool.PumpingCfg
LeanPool.PythagoreanPolynomialParametrization
LeanPool.QuasiBorelSpaces
LeanPool.RamanujanNagell
LeanPool.RamanujanTauMissesPrimes
LeanPool.Redhill
LeanPool.RiemannMappingTheorem
LeanPool.RlTheoryInLean
LeanPool.RootSystem
LeanPool.Rupert
LeanPool.SardMoreira
LeanPool.SelbergSieve4
LeanPool.SemicircleLaw
LeanPool.Sensitivity
LeanPool.SetTheory
LeanPool.Shannon1948Formalization
LeanPool.SingularModuli
LeanPool.SpecialNumbers
LeanPool.SumsThreeSquares
LeanPool.SyntheticEuclid4
LeanPool.ThreeGap
LeanPool.Turan3
LeanPool.TwoColoringOneRound
LeanPool.UnconditionalSchauderBasis
LeanPool.VirasoroProject
LeanPool.WhiteheadTheorem
LeanPool.ZFLean
LeanPool.Zeta3Irrational
LeanPool.ZetaH123
LeanPool.ZhangYeungInequality
LeanPool.ABCExceptions.ForMathlib
LeanPool.ABCExceptions.Section2
LeanPool.ABCExceptions.Section4
LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications
LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic
LeanPool.AFormalizationOfBorelDeterminacyInLean.Game
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof
LeanPool.AFormalizationOfBorelDeterminacyInLean.QualityAliases
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree
LeanPool.AgreeToDisagree.AgreeToDisagree
LeanPool.AgreeToDisagree.AgreeToDisagreeBeliefs
LeanPool.AharoniKorman.Counterexample
LeanPool.AharoniKorman.ForMathlib
LeanPool.AndersonConjecture.AdicKerEval
LeanPool.AndersonConjecture.AdicLocal
LeanPool.AndersonConjecture.AdicNoetherian
LeanPool.AndersonConjecture.Basic
LeanPool.AndersonConjecture.CompleteDomain
LeanPool.AndersonConjecture.Jensen
LeanPool.AndersonConjecture.Main
LeanPool.AndersonConjecture.QuasiCompleteRing
LeanPool.Apportionment.Basic
LeanPool.Apportionment.PlausibleInstances
LeanPool.Apportionment.Utils
LeanPool.ArchonFirstProofResults.FirstProof4
LeanPool.ArchonFirstProofResults.FirstProof6
LeanPool.ArtinWedderburn.ArtinWedderburnTheorem
LeanPool.ArtinWedderburn.Auxiliary
LeanPool.ArtinWedderburn.CornerCornerLemma
LeanPool.ArtinWedderburn.CornerRing
LeanPool.ArtinWedderburn.IdealProd
LeanPool.ArtinWedderburn.Idempotents
LeanPool.ArtinWedderburn.MatrixUnits
LeanPool.ArtinWedderburn.MinIdeals
LeanPool.ArtinWedderburn.NiceIdeals
LeanPool.ArtinWedderburn.NonUnitalToUnital
LeanPool.ArtinWedderburn.PrimeRing
LeanPool.ArtinWedderburn.SetProd
LeanPool.Biswal.Theorem1
LeanPool.Biswal.Theorem23
LeanPool.BrauerGroupNew.AbsoluteIsoH2
LeanPool.BrauerGroupNew.AlgClosedUnion
LeanPool.BrauerGroupNew.BrauerGroup
LeanPool.BrauerGroupNew.BrauerOverR
LeanPool.BrauerGroupNew.CentralSimple
LeanPool.BrauerGroupNew.Centralizer
LeanPool.BrauerGroupNew.CrossProductAlgebra
LeanPool.BrauerGroupNew.DoubleCentralizer
LeanPool.BrauerGroupNew.ExtendScalar
LeanPool.BrauerGroupNew.FieldCat
LeanPool.BrauerGroupNew.FiniteField
LeanPool.BrauerGroupNew.FrobeniusTheorem
LeanPool.BrauerGroupNew.IsoSecond
LeanPool.BrauerGroupNew.LemmasAboutSimpleRing
LeanPool.BrauerGroupNew.Mathlib
LeanPool.BrauerGroupNew.MatrixCenterEquiv
LeanPool.BrauerGroupNew.MatrixEquivTensor
LeanPool.BrauerGroupNew.MoritaEquivalence
LeanPool.BrauerGroupNew.RelativeBrauer
LeanPool.BrauerGroupNew.SkolemNoether
LeanPool.BrauerGroupNew.SplittingOfCSA
LeanPool.BrauerGroupNew.Subfield
LeanPool.BrauerGroupNew.ToSecond
LeanPool.BrauerGroupNew.TwoSidedIdeal
LeanPool.BrauerGroupNew.Wedderburn
LeanPool.BrauerGroupNew.ZeroSevenFourE
LeanPool.Brouwer.Brouwer
LeanPool.Brouwer.BrouwerProduct
LeanPool.Brouwer.Nash
LeanPool.Brouwer.Primitive
LeanPool.Brouwer.Scarf
LeanPool.Brouwer.ScarfPath
LeanPool.Brouwer.Simplex
LeanPool.BruhatTits.Cartan
LeanPool.BruhatTits.Graph
LeanPool.BruhatTits.Harmonic
LeanPool.BruhatTits.Lattice
LeanPool.BruhatTits.Utils
LeanPool.Burkholder.Majorants
LeanPool.Burkholder.MartingaleTransforms
LeanPool.CencovPetz.Basic
LeanPool.CencovPetz.CencovFinite
LeanPool.CencovPetz.CencovSplitPoint
LeanPool.CencovPetz.ContinuousExtension
LeanPool.CencovPetz.FisherContinuity
LeanPool.CencovPetz.LeftInverseIsometry
LeanPool.CencovPetz.MarkovMorphism
LeanPool.CencovPetz.MonotoneMetric
LeanPool.CencovPetz.PermutationInvariance
LeanPool.CencovPetz.PermutationInvariantBilinForm
LeanPool.CencovPetz.RationalDensity
LeanPool.CencovPetz.RationalPoint
LeanPool.CencovPetz.Replication
LeanPool.CencovPetz.ReplicationInvariance
LeanPool.CencovPetz.Simplex
LeanPool.CencovPetz.SimplexTopology
LeanPool.CencovPetz.Splitting
LeanPool.CencovPetz.SplittingInvariance
LeanPool.CencovPetz.SplittingUniform
LeanPool.CencovPetz.SufficientStatistic
LeanPool.CencovPetz.Uniform
LeanPool.CencovPetz.UniformScalarConstant
LeanPool.CencovPetz.UniformScalarMultiple
LeanPool.CencovPetz.UniformSimplex
LeanPool.CircuitComplexity.AC0
LeanPool.CircuitComplexity.AON
LeanPool.CircuitComplexity.Basic
LeanPool.CircuitComplexity.EssentialInput
LeanPool.CircuitComplexity.LowerBound
LeanPool.CircuitComplexity.NF
LeanPool.CircuitComplexity.Nondeterminism
LeanPool.CircuitComplexity.Schnorr
LeanPool.CircuitComplexity.Shannon
LeanPool.CircuitComplexity.Valiant
LeanPool.CircuitComplexity.XOR
LeanPool.Clawristotle.CoulombConcreteTheorem42
LeanPool.Clawristotle.CoulombFlux
LeanPool.Clawristotle.CoulombFluxBound
LeanPool.Clawristotle.CoulombFluxConv
LeanPool.Clawristotle.CoulombFluxDiff
LeanPool.Clawristotle.CoulombForceTransport
LeanPool.Clawristotle.CoulombKernel
LeanPool.Clawristotle.CoulombNonvacuous
LeanPool.Clawristotle.CoulombPSD
LeanPool.Clawristotle.CoulombPSDHelpers
LeanPool.Clawristotle.CoulombSpatialTransport
LeanPool.Clawristotle.Defs
LeanPool.Clawristotle.FlatTorus3Lemmas
LeanPool.Clawristotle.GaussianHelpers
LeanPool.Clawristotle.IteratedDerivHelpers
LeanPool.Clawristotle.LogBoundHelpers
LeanPool.Clawristotle.NewtonianPotential
LeanPool.Clawristotle.SchwartzDecayDefs
LeanPool.Clawristotle.Section2
LeanPool.Clawristotle.Section3
LeanPool.Clawristotle.Section3Helpers
LeanPool.Clawristotle.Section3Helpers2
LeanPool.Clawristotle.Section4
LeanPool.Clawristotle.Section5
LeanPool.Clawristotle.Section6
LeanPool.Clawristotle.Section7
LeanPool.Clawristotle.Section8
LeanPool.Clawristotle.Theorem42
LeanPool.Clawristotle.TorusDefs
LeanPool.Clawristotle.TorusInstance
LeanPool.Clawristotle.TorusIntegration
LeanPool.Clawristotle.VMLInputDerive
LeanPool.Clawristotle.VMLStructures
LeanPool.Clawristotle.VelocityDecayInstance
LeanPool.Computability.ArithHierarchy
LeanPool.Computability.AutGrp
LeanPool.Computability.Encoding
LeanPool.Computability.Jump
LeanPool.Computability.Oracle
LeanPool.Computability.TuringDegree
LeanPool.ComputableReal.AuxLemmas
LeanPool.ComputableReal.ComputableRSeq
LeanPool.ComputableReal.ComputableReal
LeanPool.ComputableReal.IsComputable
LeanPool.ComputableReal.IsComputableC
LeanPool.ComputableReal.SpecialFunctions
LeanPool.ConnesKreimer.Coassoc
LeanPool.ConnesKreimer.Core
LeanPool.ConnesKreimer.PowerSeriesLogMul
LeanPool.CriticalPortraits.Census
LeanPool.CriticalPortraits.Core
LeanPool.CriticalPortraits.CycleLemma
LeanPool.CriticalPortraits.Denominator
LeanPool.CriticalPortraits.Forward
LeanPool.CriticalPortraits.Injectivity
LeanPool.CriticalPortraits.Portraits
LeanPool.CriticalPortraits.Surjectivity
LeanPool.DeadEnds.Basic
LeanPool.DeadEnds.CRT
LeanPool.DeadEnds.Counting
LeanPool.DeadEnds.CountingBlocks
LeanPool.DeadEnds.InclusionExclusion
LeanPool.DeadEnds.PrimeTail
LeanPool.DeadEnds.RelevantPrimes
LeanPool.DeadEnds.Solution
LeanPool.DeadEnds.TailEstimates
LeanPool.DemazureOperatorsLean.Demazure
LeanPool.DemazureOperatorsLean.DemazureAux
LeanPool.DemazureOperatorsLean.DemazureAuxRelations
LeanPool.DemazureOperatorsLean.DemazureRelations
LeanPool.DemazureOperatorsLean.Matsumoto
LeanPool.DemazureOperatorsLean.StrongExchange
LeanPool.DemazureProduct.AspPerm
LeanPool.DemazureProduct.Avoiding321
LeanPool.DemazureProduct.InvSet
LeanPool.DemazureProduct.ReducedProducts
LeanPool.DemazureProduct.Reduction
LeanPool.DemazureProduct.SlipFace
LeanPool.DemazureProduct.Submodular
LeanPool.DemazureProduct.Tableaux
LeanPool.DemazureProduct.Transpositions
LeanPool.DemazureProduct.Utils
LeanPool.DemazureProduct.Valley
LeanPool.Desargues.Basic
LeanPool.Desargues.Morphism
LeanPool.Desargues.PV
LeanPool.Desargues.Structure
LeanPool.DirectedTopologyLean4.Constructions
LeanPool.DirectedTopologyLean4.CoverLemma
LeanPool.DirectedTopologyLean4.DTop
LeanPool.DirectedTopologyLean4.DihomotopyCover
LeanPool.DirectedTopologyLean4.DihomotopyFlip
LeanPool.DirectedTopologyLean4.DihomotopyToPathDihomotopy
LeanPool.DirectedTopologyLean4.Dipath
LeanPool.DirectedTopologyLean4.DipathSubtype
LeanPool.DirectedTopologyLean4.DirectedHomotopy
LeanPool.DirectedTopologyLean4.DirectedMap
LeanPool.DirectedTopologyLean4.DirectedPathHomotopy
LeanPool.DirectedTopologyLean4.DirectedSpace
LeanPool.DirectedTopologyLean4.DirectedUnitInterval
LeanPool.DirectedTopologyLean4.DirectedVanKampen
LeanPool.DirectedTopologyLean4.Fraction
LeanPool.DirectedTopologyLean4.FractionEqualities
LeanPool.DirectedTopologyLean4.FundamentalCategory
LeanPool.DirectedTopologyLean4.Interpolate
LeanPool.DirectedTopologyLean4.MonotonePath
LeanPool.DirectedTopologyLean4.MorphismAux
LeanPool.DirectedTopologyLean4.PathCover
LeanPool.DirectedTopologyLean4.PushoutAlternative
LeanPool.DirectedTopologyLean4.SplitDihomotopy
LeanPool.DirectedTopologyLean4.SplitPath
LeanPool.DirectedTopologyLean4.StretchPath
LeanPool.DirectedTopologyLean4.TransRefl
LeanPool.DirectedTopologyLean4.UnitIntervalAux
LeanPool.DomainTheory.Constructive
LeanPool.DomainTheory.InfoSys
LeanPool.Duality.Common
LeanPool.Duality.ExtendedFields
LeanPool.Duality.FarkasBartl
LeanPool.Duality.FarkasBasic
LeanPool.Duality.FarkasSpecial
LeanPool.Duality.LinearProgramming
LeanPool.Duality.LinearProgrammingB
LeanPool.Egrs75.AddBranch
LeanPool.Egrs75.BadPrefixRoute
LeanPool.Egrs75.CentralBinomialDigits
LeanPool.Egrs75.ClearingHigh
LeanPool.Egrs75.ConditionThreeWindow
LeanPool.Egrs75.Defs
LeanPool.Egrs75.DigitAtToolkit
LeanPool.Egrs75.DigitVector
LeanPool.Egrs75.Instances
LeanPool.Egrs75.KummerValuation
LeanPool.Egrs75.LeafInduction
LeanPool.Egrs75.LogIrrationality
LeanPool.Egrs75.MoveDigits
LeanPool.Egrs75.MuFinish
LeanPool.Egrs75.Reduction
LeanPool.Egrs75.RoundUp
LeanPool.Egrs75.SeedWindow
LeanPool.Egrs75.SubtractBranch
LeanPool.Erdos1196.Basic
LeanPool.Erdos1196.FirstEntryRowTerm
LeanPool.Erdos1196.FormalConjecturesErdos1196
LeanPool.Erdos1196.HitMass
LeanPool.Erdos1196.Main
LeanPool.Erdos1196.Markov
LeanPool.Erdos1196.Normalization
LeanPool.Erdos1196.NormalizationCore
LeanPool.Erdos1196.NormalizationSmallPrime
LeanPool.Erdos1196.Preliminaries
LeanPool.Erdos1196.PreliminariesMertens
LeanPool.Erdos1196.PreliminariesTailAux
LeanPool.Erdos1196.PrimitiveWeight
LeanPool.Erdos137.AxiomAudit
LeanPool.Erdos137.Base
LeanPool.Erdos137.BlockFramework
LeanPool.Erdos137.CombinedSplice
LeanPool.Erdos137.Finiteness
LeanPool.Erdos137.JointFiniteness
LeanPool.Erdos137.QuarticCrude
LeanPool.Erdos137.RefinedOverlap
LeanPool.Erdos137.RoughPartStructure
LeanPool.Erdos137.SexticCrude
LeanPool.Erdos137.SmoothRefinement
LeanPool.Erdos137.SpliceFiniteness
LeanPool.Erdos137.SquarefreeCapacity
LeanPool.Erdos137.TaoPoint
LeanPool.Erdos367.Core139
LeanPool.Erdos367.Core4027
LeanPool.Erdos367.GeneralKUpperBound
LeanPool.Erdos367.K3AbcUpperBound
LeanPool.Erdos367.PellLimsup
LeanPool.Erdos367.RFullLowerBound
LeanPool.Erdos403.Basic
LeanPool.Erdos403.FactBase
LeanPool.Erdos403.Sharp
LeanPool.ErdosTuzaValtr.All
LeanPool.EventStructures.Basic
LeanPool.EventStructures.Computation
LeanPool.EventStructures.Configuration
LeanPool.EventStructures.FinitePoset
LeanPool.EventStructures.Log
LeanPool.EventStructures.Path
LeanPool.EventStructures.Replay
LeanPool.EventStructures.Rollback
LeanPool.EventStructures.Trace
LeanPool.FactorizationSystems.Basic
LeanPool.FactorizationSystems.Characterization
LeanPool.FactorizationSystems.Examples
LeanPool.FactorizationSystems.OrthogonalComplements
LeanPool.FactorizationSystems.Orthogonality
LeanPool.FelConjecture.Solution
LeanPool.Fineqs.Main
LeanPool.FiveEighthsTheorem.Basic
LeanPool.Flean.Basic
LeanPool.Flean.FloatCfg
LeanPool.Flean.FloatRep
LeanPool.Flean.IntRounding
LeanPool.Flean.LogRules
LeanPool.Flean.Rounding
LeanPool.Flean.Subnorm
LeanPool.FoZfc.Axioms
LeanPool.FoZfc.Basic
LeanPool.FoZfc.BoundedFormulaOps
LeanPool.FoZfc.FixedSnoc
LeanPool.FoZfc.Replacement
LeanPool.FoZfc.Tostring
LeanPool.FormalLearningTheory.Basic
LeanPool.FormalLearningTheory.Bridge
LeanPool.FormalLearningTheory.Complexity
LeanPool.FormalLearningTheory.Computation
LeanPool.FormalLearningTheory.Criterion
LeanPool.FormalLearningTheory.Data
LeanPool.FormalLearningTheory.Learner
LeanPool.FormalLearningTheory.Process
LeanPool.FormalLearningTheory.Theorem
LeanPool.FormalizationOfBoundedArithmetic.Algebra
LeanPool.FormalizationOfBoundedArithmetic.AxiomSchemes
LeanPool.FormalizationOfBoundedArithmetic.BasicSingleSorted
LeanPool.FormalizationOfBoundedArithmetic.Complexity
LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables
LeanPool.FormalizationOfBoundedArithmetic.IDelta0
LeanPool.FormalizationOfBoundedArithmetic.IOPEN
LeanPool.FormalizationOfBoundedArithmetic.IsEnum
LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano
LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella
LeanPool.FormalizationOfBoundedArithmetic.MathlibSimps
LeanPool.FormalizationOfBoundedArithmetic.Order
LeanPool.FormalizationOfBoundedArithmetic.Register
LeanPool.FormalizationOfBoundedArithmetic.Semantics
LeanPool.FormalizationOfBoundedArithmetic.SimpRules
LeanPool.FormalizationOfBoundedArithmetic.Syntax
LeanPool.FormalizationOfBoundedArithmetic.V0
LeanPool.FormalizationOfBoundedArithmetic.V0StrAddAssoc
LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm
LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc
LeanPool.ForwardEuler.Main
LeanPool.FriezePatterns.Chapter1
LeanPool.FriezePatterns.Chapter2
LeanPool.FriezePatterns.Chapter3
LeanPool.FrontierMathOpenHypergraphs.Basic
LeanPool.FrontierMathOpenHypergraphs.Lubell
LeanPool.FrontierMathOpenHypergraphs.Substitution
LeanPool.FrontierMathOpenHypergraphs.Uniform
LeanPool.GrothendieckVanishing.ClosedImmersion
LeanPool.GrothendieckVanishing.ClosedImmersionCohomology
LeanPool.GrothendieckVanishing.CohomologyAPI
LeanPool.GrothendieckVanishing.ConstantSheafFlasque
LeanPool.GrothendieckVanishing.FinitelyGeneratedVanishing
LeanPool.GrothendieckVanishing.FlasqueVanishing
LeanPool.GrothendieckVanishing.GeneratedSubsheaf
LeanPool.GrothendieckVanishing.GrothendieckVanishing
LeanPool.GrothendieckVanishing.GrothendieckVanishingOverview
LeanPool.GrothendieckVanishing.IrreducibleStep
LeanPool.GrothendieckVanishing.PresheafFilteredColimit
LeanPool.GrothendieckVanishing.PresheafFilteredColimitCore
LeanPool.GrothendieckVanishing.PresheafFilteredColimitGeneral
LeanPool.GrothendieckVanishing.TopologicalKrullDim
LeanPool.GrothendieckVanishing.ZeroOutside
LeanPool.HSDInteriorPointLP.FixedYTMTheory
LeanPool.HSDInteriorPointLP.GeneratedConvergence
LeanPool.HSDInteriorPointLP.LocalNeighborhoodEstimates
LeanPool.HSDInteriorPointLP.NewtonSystem
LeanPool.HSDInteriorPointLP.PrimalDualData
LeanPool.IsTranscendentalPi.AnalyticEstimates
LeanPool.IsTranscendentalPi.CalculusOnPoly
LeanPool.IsTranscendentalPi.ComplexExponential
LeanPool.IsTranscendentalPi.IncrementalDerivatives
LeanPool.IsTranscendentalPi.Main
LeanPool.IsTranscendentalPi.NivenPolynomials
LeanPool.IsTranscendentalPi.ScaledAuxiliaryPolynomial
LeanPool.IsTranscendentalPi.SubsetSumPolynomial
LeanPool.IsTranscendentalPi.SymmetricPolynomials
LeanPool.Isoperimetric.Basic
LeanPool.Isoperimetric.BrunnMinkowski
LeanPool.Isoperimetric.Isoperimetric
LeanPool.Isoperimetric.PrekopaLeindler
LeanPool.KaltonRoberts.Collections
LeanPool.KaltonRoberts.Defs
LeanPool.KaltonRoberts.DualCert
LeanPool.KaltonRoberts.EpsilonRecombination
LeanPool.KaltonRoberts.Intersections
LeanPool.KaltonRoberts.Lemmas
LeanPool.KaltonRoberts.LogBounds
LeanPool.KaltonRoberts.MainTheorem
LeanPool.KaltonRoberts.Numerical
LeanPool.KaltonRoberts.PhiAnalysis
LeanPool.KaltonRoberts.PhiDeriv
LeanPool.KaltonRoberts.Pipeline
LeanPool.KaltonRoberts.PipelineEps
LeanPool.KaltonRoberts.Pippenger
LeanPool.KaltonRoberts.PippengerProof
LeanPool.KaltonRoberts.Recombination
LeanPool.KaltonRoberts.UniformRecombination
LeanPool.KrafftSieve.Basic
LeanPool.KrafftSieve.Defs
LeanPool.KrafftSieve.MainTheorem
LeanPool.KrafftSieve.OptimalWeights
LeanPool.KrafftSieve.SelbergWeights
LeanPool.KrafftSieve.ThirdHarmonic
LeanPool.KrafftSieve.Variance
LeanPool.LatticeTriangle.Solution
LeanPool.Lean4Itree.ITree
LeanPool.Lean4Itree.Paco
LeanPool.LeanBooleanfun.Arrow
LeanPool.LeanBooleanfun.AuxLemmas
LeanPool.LeanBooleanfun.Basic
LeanPool.LeanBooleanfun.BooleanValued
LeanPool.LeanBooleanfun.ToMathlib
LeanPool.LeanComplexAnalysis.Harmonic
LeanPool.LeanComplexAnalysis.UnivalentFunctions
LeanPool.LeanModelChecking.ABW
LeanPool.LeanModelChecking.ABWNBW
LeanPool.LeanModelChecking.LTLNBWResult
LeanPool.LeanModelChecking.LTLNBWStatement
LeanPool.LeanModelChecking.LTLNNF
LeanPool.LeanModelChecking.NNFABW
LeanPool.LeanModelChecking.SafetyLivenessDecomposition
LeanPool.LeanPolyABC.All
LeanPool.LeanPolyABC.MasonStothers
LeanPool.LeanQuantumAlg.Algorithms
LeanPool.LeanQuantumAlg.Core
LeanPool.LeanQuantumAlg.Init
LeanPool.LeanQuantumAlg.Primitives
LeanPool.LeanQuantumAlg.Util
LeanPool.Lentil.Basic
LeanPool.Lentil.Expr
LeanPool.Lentil.Foldable
LeanPool.Lentil.Util
LeanPool.LowDimSolvClassification.Classification1
LeanPool.LowDimSolvClassification.Classification2
LeanPool.LowDimSolvClassification.Classification3
LeanPool.LowDimSolvClassification.GeneralResults
LeanPool.LowDimSolvClassification.InstancesConstructions
LeanPool.LowDimSolvClassification.InstancesLowDim
LeanPool.LowDimSolvClassification.LemmasDim3
LeanPool.LowDimSolvClassification.QuotientSolvable
LeanPool.LowDimSolvClassification.Semidirect
LeanPool.LowDimSolvClassification.Tactics
LeanPool.MRiscX.Basic
LeanPool.MisereGames.AugmentedForm
LeanPool.MisereGames.Form
LeanPool.MisereGames.GameForm
LeanPool.MisereGames.GameGraph
LeanPool.MisereGames.OfSets
LeanPool.MisereGames.Outcome
LeanPool.MisereGames.Player
LeanPool.MisereGames.Ruleset
LeanPool.Monlib4.LinearAlgebra
LeanPool.Monlib4.Monlib
LeanPool.Monlib4.Other
LeanPool.Monlib4.Preq
LeanPool.Monlib4.QuantumGraph
LeanPool.Monlib4.RepTheory
LeanPool.Monsky.Appendix
LeanPool.Monsky.BasicDefinitions
LeanPool.Monsky.MainStatement
LeanPool.Monsky.Miscellaneous
LeanPool.Monsky.MonskyEven
LeanPool.Monsky.RainbowTriangles
LeanPool.Monsky.SegmentCounting
LeanPool.Monsky.SegmentTriangle
LeanPool.Monsky.SimplexBasic
LeanPool.Monsky.Square
LeanPool.Monsky.TriangleCorollary
LeanPool.Neukirch.ExtensionOfDedekindDomains
LeanPool.Neukirch.HilbertRamificationTheory
LeanPool.OSforGFF.Bochner
LeanPool.OSforGFF.Covariance
LeanPool.OSforGFF.GaussianField
LeanPool.OSforGFF.General
LeanPool.OSforGFF.KolmogorovExtension4
LeanPool.OSforGFF.Measure
LeanPool.OSforGFF.Minlos
LeanPool.OSforGFF.OS
LeanPool.OSforGFF.Schwinger
LeanPool.OSforGFF.Spacetime
LeanPool.OrderPQ.Basic
LeanPool.OrderPQ.IsCyclic
LeanPool.OrderPQ.Main
LeanPool.OrderPQ.MonoidHom
LeanPool.OrderPQ.MulZMod
LeanPool.OrderPQ.PrimeOrder
LeanPool.OrderPQ.SemidirectProduct
LeanPool.OrderPQ.TorsionBy
LeanPool.PCFTheory.Background
LeanPool.PCFTheory.ClubGuessing
LeanPool.PLAcceleratedNesterovLean.Convergence
LeanPool.PLAcceleratedNesterovLean.Core
LeanPool.PLAcceleratedNesterovLean.MainTheorem
LeanPool.PLAcceleratedNesterovLean.MorseBott
LeanPool.PartialCombinatoryAlgebras.Basic
LeanPool.PartialCombinatoryAlgebras.CombinatoryAlgebra
LeanPool.PartialCombinatoryAlgebras.FreeCombinatoryAlgebra
LeanPool.PartialCombinatoryAlgebras.GraphModel
LeanPool.PartialCombinatoryAlgebras.PartialCombinatoryAlgebra
LeanPool.PartialCombinatoryAlgebras.Programming
LeanPool.PartialRegularity.Extension
LeanPool.PebblingLean.Basic
LeanPool.PebblingLean.Concentration
LeanPool.PebblingLean.Delivery
LeanPool.PebblingLean.Examples
LeanPool.PebblingLean.FiniteProbability
LeanPool.PebblingLean.GraphIso
LeanPool.PebblingLean.Hypercube
LeanPool.PebblingLean.HypercubePath
LeanPool.PebblingLean.HypercubeProduct
LeanPool.PebblingLean.LowerBound
LeanPool.PebblingLean.Paper
LeanPool.PebblingLean.Product
LeanPool.PebblingLean.UpperBound
LeanPool.PebblingLean.UpperBoundDelivery
LeanPool.PebblingLean.UpperBoundLoss
LeanPool.PebblingLean.UpperBoundParameters
LeanPool.PebblingLean.UpperBoundProbability
LeanPool.PebblingLean.UpperBoundRecurrence
LeanPool.PebblingLean.Weight
LeanPool.PentagonalNumberTheorem.Complex
LeanPool.PentagonalNumberTheorem.Generic
LeanPool.PentagonalNumberTheorem.Old
LeanPool.PentagonalNumberTheorem.Partition
LeanPool.PentagonalNumberTheorem.PowerSeries
LeanPool.PhaseRetrieval.Constant
LeanPool.PhaseRetrieval.DimdPoly
LeanPool.PointwiseBirkhoff.Main
LeanPool.PolyaEnumerationTheorem.Basic
LeanPool.PolyaEnumerationTheorem.Concrete
LeanPool.PolyaEnumerationTheorem.PermutationAuxiliary
LeanPool.PolyaEnumerationTheorem.ReductionToFin
LeanPool.PolyaEnumerationTheorem.StirlingFirstKindSum
LeanPool.Polylean.Complexes
LeanPool.Polylean.ConjInvLength
LeanPool.Polylean.Polymath
LeanPool.Polylean.UnitConjecture
LeanPool.PolynomialMethodRestrictedSums.ANRPolynomialMethod
LeanPool.PolynomialMethodRestrictedSums.CauchyDavenportTheorem
LeanPool.PolynomialMethodRestrictedSums.CompressedSizesRestrictedSum
LeanPool.PolynomialMethodRestrictedSums.DiasDaSilvaHamidoune
LeanPool.PolynomialMethodRestrictedSums.RestrictedSumDistinctSizes
LeanPool.PolynomialMethodRestrictedSums.VandermondeCoefficientFormula
LeanPool.Polytopes.Cutspace
LeanPool.Polytopes.Halfspace
LeanPool.Polytopes.MainTheorem
LeanPool.Polytopes.Polar
LeanPool.Polytopes.Polytope
LeanPool.Polytopes.Pre
LeanPool.PumpingCfg.ParseTree
LeanPool.PumpingCfg.Pumping
LeanPool.PumpingCfg.ToMathlib
LeanPool.PumpingCfg.Utils
LeanPool.PythagoreanPolynomialParametrization.Basic
LeanPool.PythagoreanPolynomialParametrization.Explanatory
LeanPool.PythagoreanPolynomialParametrization.IntegerValued
LeanPool.PythagoreanPolynomialParametrization.Main
LeanPool.PythagoreanPolynomialParametrization.Obstructions
LeanPool.PythagoreanPolynomialParametrization.Positive
LeanPool.PythagoreanPolynomialParametrization.SourceLemmas
LeanPool.QuasiBorelSpaces.Basic
LeanPool.QuasiBorelSpaces.Chain
LeanPool.QuasiBorelSpaces.Cont
LeanPool.QuasiBorelSpaces.Defs
LeanPool.QuasiBorelSpaces.ENNReal
LeanPool.QuasiBorelSpaces.Finset
LeanPool.QuasiBorelSpaces.FlatReal
LeanPool.QuasiBorelSpaces.Functor
LeanPool.QuasiBorelSpaces.Hom
LeanPool.QuasiBorelSpaces.IsHomDiagonal
LeanPool.QuasiBorelSpaces.Lift
LeanPool.QuasiBorelSpaces.List
LeanPool.QuasiBorelSpaces.MeasureTheory
LeanPool.QuasiBorelSpaces.Multiset
LeanPool.QuasiBorelSpaces.Nat
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder
LeanPool.QuasiBorelSpaces.OmegaHom
LeanPool.QuasiBorelSpaces.OmegaQuasiBorelSpace
LeanPool.QuasiBorelSpaces.Option
LeanPool.QuasiBorelSpaces.Pi
LeanPool.QuasiBorelSpaces.PreProbabilityMeasure
LeanPool.QuasiBorelSpaces.ProbabilityMeasure
LeanPool.QuasiBorelSpaces.Prod
LeanPool.QuasiBorelSpaces.Prop
LeanPool.QuasiBorelSpaces.Quotient
LeanPool.QuasiBorelSpaces.Rose
LeanPool.QuasiBorelSpaces.RoseTree
LeanPool.QuasiBorelSpaces.SeparatesPoints
LeanPool.QuasiBorelSpaces.Sigma
LeanPool.QuasiBorelSpaces.Subtype
LeanPool.QuasiBorelSpaces.Sum
LeanPool.QuasiBorelSpaces.UnitInterval
LeanPool.RamanujanNagell.Basic
LeanPool.RamanujanNagell.Helpers
LeanPool.RamanujanTauMissesPrimes.Solution
LeanPool.Redhill.BB94
LeanPool.Redhill.KonyaginPrelude
LeanPool.RiemannMappingTheorem.Cindex
LeanPool.RiemannMappingTheorem.Defs
LeanPool.RiemannMappingTheorem.DerivInj
LeanPool.RiemannMappingTheorem.Etape2
LeanPool.RiemannMappingTheorem.HasSqrt
LeanPool.RiemannMappingTheorem.Hurwitz
LeanPool.RiemannMappingTheorem.Main
LeanPool.RiemannMappingTheorem.Montel
LeanPool.RiemannMappingTheorem.Spaces
LeanPool.RiemannMappingTheorem.ToMathlib
LeanPool.RiemannMappingTheorem.Uniform
LeanPool.RlTheoryInLean.Analysis
LeanPool.RlTheoryInLean.Data
LeanPool.RlTheoryInLean.Defs
LeanPool.RlTheoryInLean.MeasureTheory
LeanPool.RlTheoryInLean.Order
LeanPool.RlTheoryInLean.Probability
LeanPool.RlTheoryInLean.StochasticApproximation
LeanPool.RootSystem.An
LeanPool.RootSystem.BCn
LeanPool.Rupert.Affine
LeanPool.Rupert.Attr
LeanPool.Rupert.Basic
LeanPool.Rupert.Convex
LeanPool.Rupert.Cube
LeanPool.Rupert.FinCases
LeanPool.Rupert.Icosahedron
LeanPool.Rupert.MatrixSimps
LeanPool.Rupert.Quaternion
LeanPool.Rupert.Set
LeanPool.Rupert.SnubCube
LeanPool.Rupert.Square
LeanPool.Rupert.Tetrahedron
LeanPool.Rupert.TriakisTetrahedron
LeanPool.SardMoreira.Chart
LeanPool.SardMoreira.ChartEstimates
LeanPool.SardMoreira.ContDiff
LeanPool.SardMoreira.ContDiffMoreiraHolder
LeanPool.SardMoreira.ContinuousMultilinearMap
LeanPool.SardMoreira.ImplicitFunction
LeanPool.SardMoreira.LebesgueDensity
LeanPool.SardMoreira.LinearAlgebra
LeanPool.SardMoreira.LocalEstimates
LeanPool.SardMoreira.MainTheorem
LeanPool.SardMoreira.MeasureBallSemicontinuous
LeanPool.SardMoreira.MeasureComap
LeanPool.SardMoreira.MeasureNNReal
LeanPool.SardMoreira.NormedSpace
LeanPool.SardMoreira.OuterMeasureDeriv
LeanPool.SardMoreira.ToMathlib
LeanPool.SardMoreira.Topology
LeanPool.SardMoreira.UnifDoublingCover
LeanPool.SardMoreira.Unused
LeanPool.SardMoreira.UpperLowerSemicontinuous
LeanPool.SardMoreira.WithRPowDist
LeanPool.SelbergSieve4.Applications
LeanPool.SelbergSieve4.AuxResults
LeanPool.SelbergSieve4.ForArithmeticFunction
LeanPool.SelbergSieve4.ForMathlib
LeanPool.SelbergSieve4.MainResults
LeanPool.SelbergSieve4.Selberg
LeanPool.SelbergSieve4.SieveLemmas
LeanPool.SelbergSieve4.Tactic
LeanPool.SelbergSieve4.UpperBoundSieve
LeanPool.SemicircleLaw.SemicircleDistribution
LeanPool.Sensitivity.Basic
LeanPool.Sensitivity.Consequences
LeanPool.Sensitivity.Defs
LeanPool.Sensitivity.HuangBridge
LeanPool.Sensitivity.Main
LeanPool.Sensitivity.Multilinear
LeanPool.Sensitivity.Parity
LeanPool.Sensitivity.Subcube
LeanPool.SetTheory.Basic
LeanPool.SetTheory.ElementaryEmbedding
LeanPool.SetTheory.KunenInconsistency
LeanPool.SetTheory.Omega
LeanPool.SetTheory.OrderTheory
LeanPool.SetTheory.Ordinals
LeanPool.SetTheory.Realize
LeanPool.SetTheory.SimpAttr
LeanPool.Shannon1948Formalization.Entropy
LeanPool.SpecialNumbers.Euclidian
LeanPool.SpecialNumbers.Eulerian
LeanPool.SpecialNumbers.Sylvester
LeanPool.SumsThreeSquares.MinkowskiConvex
LeanPool.SumsThreeSquares.SumThreeSquares
LeanPool.SyntheticEuclid4.Axioms
LeanPool.SyntheticEuclid4.PermTactics
LeanPool.SyntheticEuclid4.SyntheticEuclid4
LeanPool.SyntheticEuclid4.Tactics
LeanPool.ThreeGap.ChevallierCount
LeanPool.ThreeGap.ChevallierGapBound
LeanPool.ThreeGap.DeltaCost
LeanPool.ThreeGap.EuclideanAngle
LeanPool.ThreeGap.EuclideanDefect
LeanPool.ThreeGap.EuclideanFiveDistanceSharp
LeanPool.ThreeGap.EuclideanFiveDistanceSharpArith
LeanPool.ThreeGap.EuclideanGrowth
LeanPool.ThreeGap.EuclideanGrowthFive
LeanPool.ThreeGap.EuclideanGrowthFour
LeanPool.ThreeGap.EuclideanNN
LeanPool.ThreeGap.EuclideanPacking
LeanPool.ThreeGap.EuclideanRecords
LeanPool.ThreeGap.FiveDistance
LeanPool.ThreeGap.FiveDistanceHM
LeanPool.ThreeGap.LinftyFiveDistanceSharpArith
LeanPool.ThreeGap.LinftyThreeTorusNine
LeanPool.ThreeGap.ModTwoGrowth
LeanPool.ThreeGap.SimultaneousApprox
LeanPool.ThreeGap.SimultaneousDirichlet
LeanPool.ThreeGap.SupNormGrowth
LeanPool.ThreeGap.TorusReduction
LeanPool.Turan3.Turans3rdProof
LeanPool.TwoColoringOneRound.API
LeanPool.TwoColoringOneRound.Definitions
LeanPool.TwoColoringOneRound.LowerBound
LeanPool.TwoColoringOneRound.MainResults
LeanPool.TwoColoringOneRound.Reduction
LeanPool.TwoColoringOneRound.SimpleBounds
LeanPool.TwoColoringOneRound.UpperBound
LeanPool.VirasoroProject.CentralChargeCalc
LeanPool.VirasoroProject.CentralExtension
LeanPool.VirasoroProject.Commutator
LeanPool.VirasoroProject.CyclicTripleSum
LeanPool.VirasoroProject.FockSpace
LeanPool.VirasoroProject.FockSpaceSugawara
LeanPool.VirasoroProject.HeisenbergAlgebra
LeanPool.VirasoroProject.IndexTri
LeanPool.VirasoroProject.IsCentralExtension
LeanPool.VirasoroProject.LieAlgebraModuleUEA
LeanPool.VirasoroProject.LieAlgebraRepresentationOfBasis
LeanPool.VirasoroProject.LieCohomologySmallDegree
LeanPool.VirasoroProject.LieVerma
LeanPool.VirasoroProject.SectionSES
LeanPool.VirasoroProject.Sugawara
LeanPool.VirasoroProject.ToMathlib
LeanPool.VirasoroProject.VermaModule
LeanPool.VirasoroProject.VirasoroAlgebra
LeanPool.VirasoroProject.VirasoroCocycle
LeanPool.VirasoroProject.VirasoroVerma
LeanPool.VirasoroProject.WittAlgebra
LeanPool.VirasoroProject.WittAlgebraCohomology
LeanPool.WhiteheadTheorem.Auxiliary
LeanPool.WhiteheadTheorem.Basic
LeanPool.WhiteheadTheorem.Defs
LeanPool.WhiteheadTheorem.Exponential
LeanPool.ZFLean.Basic
LeanPool.ZFLean.Booleans
LeanPool.ZFLean.Embeddings
LeanPool.ZFLean.Functions
LeanPool.ZFLean.Integers
LeanPool.ZFLean.Isomorphisms
LeanPool.ZFLean.IsomorphismsFunsToPowRel
LeanPool.ZFLean.IsomorphismsZFNatIso
LeanPool.ZFLean.Naturals
LeanPool.ZFLean.Rationals
LeanPool.ZFLean.Sum
LeanPool.ZFLean.Tactics
LeanPool.Zeta3Irrational.Basic
LeanPool.Zeta3Irrational.Bound
LeanPool.Zeta3Irrational.Chebyshev
LeanPool.Zeta3Irrational.D
LeanPool.Zeta3Irrational.Equality
LeanPool.Zeta3Irrational.Integral
LeanPool.Zeta3Irrational.LegendrePoly
LeanPool.Zeta3Irrational.LinearForm
LeanPool.ZetaH123.H1
LeanPool.ZetaH123.H2
LeanPool.ZetaH123.H3
LeanPool.ZetaH123.Lem41
LeanPool.ZhangYeungInequality.CopyLemma
LeanPool.ZhangYeungInequality.Delta
LeanPool.ZhangYeungInequality.EntropyRegion
LeanPool.ZhangYeungInequality.Prelude
LeanPool.ZhangYeungInequality.Test
LeanPool.ZhangYeungInequality.Theorem2
LeanPool.ZhangYeungInequality.Theorem3
LeanPool.ZhangYeungInequality.Theorem4
LeanPool.ZhangYeungInequality.Theorem5
LeanPool.ABCExceptions.ForMathlib.Misc
LeanPool.ABCExceptions.ForMathlib.RingTheory
LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Choquet
LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.General
LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Meager
LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.RegularOpen
LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.FinLists
LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.General
LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.InfLists
LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.InvLimitNat
LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.Meta
LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.MiscCat
LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.BuildStrategies
LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.GaleStewart
LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Games
LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Player
LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Strategies
LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Undetermined
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BorelDeterminacy
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BuildLevelwise
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Covering
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringClosedGame
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringLim
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.WinAsap
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.BodyFunctor
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.LenTreeHom
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.PointedTrees
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.RestrictTree
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeBody
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeExtensions
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeLim
LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.Trees
LeanPool.AharoniKorman.ForMathlib.Misc
LeanPool.AndersonConjecture.CompleteDomain.CompleteDomain
LeanPool.AndersonConjecture.CompleteDomain.Domain
LeanPool.AndersonConjecture.CompleteDomain.LocalRing
LeanPool.AndersonConjecture.Jensen.Adjoin
LeanPool.AndersonConjecture.Jensen.Application
LeanPool.AndersonConjecture.Jensen.Avoidance
LeanPool.AndersonConjecture.Jensen.CloseUp
LeanPool.AndersonConjecture.Jensen.CombinedStep
LeanPool.AndersonConjecture.Jensen.Construction
LeanPool.AndersonConjecture.Jensen.Defs
LeanPool.AndersonConjecture.Jensen.Jensen
LeanPool.AndersonConjecture.Jensen.KrullDomain
LeanPool.AndersonConjecture.Jensen.NSubring
LeanPool.AndersonConjecture.Jensen.TransfiniteUnion
LeanPool.AndersonConjecture.QuasiCompleteRing.Complete
LeanPool.AndersonConjecture.QuasiCompleteRing.QuasiCompleteRing
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary
LeanPool.ArchonFirstProofResults.FirstProof4.Problem4
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary
LeanPool.ArchonFirstProofResults.FirstProof6.Problem6
LeanPool.BrauerGroupNew.Azumaya.Basic
LeanPool.BrauerGroupNew.Azumaya.Mul
LeanPool.BrauerGroupNew.Mathlib.Algebra
LeanPool.BrauerGroupNew.Mathlib.Data
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra
LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory
LeanPool.BrauerGroupNew.Mathlib.RingTheory
LeanPool.BrauerGroupNew.Morita.ChangeOfRings
LeanPool.BrauerGroupNew.Morita.TensorProduct
LeanPool.BrauerGroupNew.Subfield.Defs
LeanPool.BrauerGroupNew.Subfield.FiniteDimensional
LeanPool.BrauerGroupNew.Subfield.Separable
LeanPool.BrauerGroupNew.Subfield.Splitting
LeanPool.BrauerGroupNew.Subfield.Subfield
LeanPool.BruhatTits.Cartan.Existence
LeanPool.BruhatTits.Cartan.Uniqueness
LeanPool.BruhatTits.Graph.Edges
LeanPool.BruhatTits.Graph.Graph
LeanPool.BruhatTits.Graph.GroupAction
LeanPool.BruhatTits.Graph.Orientation
LeanPool.BruhatTits.Graph.Regular
LeanPool.BruhatTits.Graph.Tree
LeanPool.BruhatTits.Graph.Vertices
LeanPool.BruhatTits.Harmonic.Application
LeanPool.BruhatTits.Harmonic.Basic
LeanPool.BruhatTits.Lattice.Basic
LeanPool.BruhatTits.Lattice.Construction
LeanPool.BruhatTits.Lattice.Distance
LeanPool.BruhatTits.Lattice.Quotient
LeanPool.BruhatTits.Lattice.Transvect
LeanPool.BruhatTits.Utils.GLSubmoduleAction
LeanPool.BruhatTits.Utils.GraphAction
LeanPool.BruhatTits.Utils.LinearAlgebra
LeanPool.BruhatTits.Utils.List
LeanPool.BruhatTits.Utils.Matrix
LeanPool.BruhatTits.Utils.Misc
LeanPool.BruhatTits.Utils.Order
LeanPool.BruhatTits.Utils.RingHom
LeanPool.BruhatTits.Utils.Subring
LeanPool.BruhatTits.Utils.ValuationRings
LeanPool.Burkholder.Majorants.Definitions
LeanPool.Burkholder.Majorants.MajorantPEq2
LeanPool.Burkholder.Majorants.MajorantPG2
LeanPool.Burkholder.Majorants.MajorantPL2
LeanPool.CircuitComplexity.AC0.Defs
LeanPool.CircuitComplexity.AON.Defs
LeanPool.CircuitComplexity.Digraph.Defs
LeanPool.CircuitComplexity.Internal.AON
LeanPool.CircuitComplexity.Internal.Bridge
LeanPool.CircuitComplexity.Internal.CircDesc
LeanPool.CircuitComplexity.Internal.LowerBound
LeanPool.CircuitComplexity.Internal.NF
LeanPool.CircuitComplexity.Internal.Nondeterminism
LeanPool.CircuitComplexity.Internal.Schnorr
LeanPool.CircuitComplexity.Internal.ShannonUpper
LeanPool.CircuitComplexity.Internal.Simulation
LeanPool.CircuitComplexity.Internal.Valiant
LeanPool.CircuitComplexity.NF.Defs
LeanPool.CircuitComplexity.Nondeterminism.Defs
LeanPool.Circuitlib.Circuit.Basic
LeanPool.Circuitlib.Circuit.Combinational
LeanPool.Circuitlib.Circuit.Gate
LeanPool.Circuitlib.Circuit.Wires
LeanPool.CompactSpectral.Topology.WeakHilbertCompact
LeanPool.ComputableReal.SpecialFunctions.Basic
LeanPool.ComputableReal.SpecialFunctions.Exp
LeanPool.ComputableReal.SpecialFunctions.Pi
LeanPool.ComputableReal.SpecialFunctions.Sqrt
LeanPool.DirectedTopologyLean4.SplitPath.SplitDipath
LeanPool.DirectedTopologyLean4.SplitPath.SplitPath
LeanPool.DirectedTopologyLean4.SplitPath.SplitProperties
LeanPool.DomainTheory.ContinuousLattice.Constructions
LeanPool.DomainTheory.ContinuousLattice.FunctionSpaceTower
LeanPool.DomainTheory.ContinuousLattice.FunctionSpaces
LeanPool.DomainTheory.ContinuousLattice.Injective
LeanPool.DomainTheory.ContinuousLattice.InverseLimits
LeanPool.DomainTheory.ContinuousLattice.MilnerCorrection
LeanPool.DomainTheory.ContinuousLattice.ScottMaps
LeanPool.DomainTheory.ContinuousLattice.Specialization
LeanPool.DomainTheory.ContinuousLattice.Theorem212
LeanPool.DomainTheory.ContinuousLattice.WayBelow
LeanPool.DomainTheory.Neighborhood.Approximable
LeanPool.DomainTheory.Neighborhood.ApproximableExercises
LeanPool.DomainTheory.Neighborhood.Basic
LeanPool.DomainTheory.Neighborhood.Definition610
LeanPool.DomainTheory.Neighborhood.Definition613
LeanPool.DomainTheory.Neighborhood.Definition63
LeanPool.DomainTheory.Neighborhood.Definition68
LeanPool.DomainTheory.Neighborhood.Definition71
LeanPool.DomainTheory.Neighborhood.Definition72
LeanPool.DomainTheory.Neighborhood.Example12
LeanPool.DomainTheory.Neighborhood.Example13
LeanPool.DomainTheory.Neighborhood.Example14
LeanPool.DomainTheory.Neighborhood.Example15
LeanPool.DomainTheory.Neighborhood.Example23
LeanPool.DomainTheory.Neighborhood.Example24
LeanPool.DomainTheory.Neighborhood.Example43
LeanPool.DomainTheory.Neighborhood.Example44
LeanPool.DomainTheory.Neighborhood.Example61
LeanPool.DomainTheory.Neighborhood.Example62
LeanPool.DomainTheory.Neighborhood.Example62A
LeanPool.DomainTheory.Neighborhood.Example62C
LeanPool.DomainTheory.Neighborhood.Example62Regular
LeanPool.DomainTheory.Neighborhood.ExampleB
LeanPool.DomainTheory.Neighborhood.Exercise112
LeanPool.DomainTheory.Neighborhood.Exercise113
LeanPool.DomainTheory.Neighborhood.Exercise114
LeanPool.DomainTheory.Neighborhood.Exercise115
LeanPool.DomainTheory.Neighborhood.Exercise116
LeanPool.DomainTheory.Neighborhood.Exercise117
LeanPool.DomainTheory.Neighborhood.Exercise118
LeanPool.DomainTheory.Neighborhood.Exercise119
LeanPool.DomainTheory.Neighborhood.Exercise120
LeanPool.DomainTheory.Neighborhood.Exercise121
LeanPool.DomainTheory.Neighborhood.Exercise122
LeanPool.DomainTheory.Neighborhood.Exercise123
LeanPool.DomainTheory.Neighborhood.Exercise124
LeanPool.DomainTheory.Neighborhood.Exercise125
LeanPool.DomainTheory.Neighborhood.Exercise126
LeanPool.DomainTheory.Neighborhood.Exercise127
LeanPool.DomainTheory.Neighborhood.Exercise213
LeanPool.DomainTheory.Neighborhood.Exercise214
LeanPool.DomainTheory.Neighborhood.Exercise215
LeanPool.DomainTheory.Neighborhood.Exercise216
LeanPool.DomainTheory.Neighborhood.Exercise218
LeanPool.DomainTheory.Neighborhood.Exercise220
LeanPool.DomainTheory.Neighborhood.Exercise221
LeanPool.DomainTheory.Neighborhood.Exercise222
LeanPool.DomainTheory.Neighborhood.Exercise314
LeanPool.DomainTheory.Neighborhood.Exercise315
LeanPool.DomainTheory.Neighborhood.Exercise316
LeanPool.DomainTheory.Neighborhood.Exercise317
LeanPool.DomainTheory.Neighborhood.Exercise318
LeanPool.DomainTheory.Neighborhood.Exercise319
LeanPool.DomainTheory.Neighborhood.Exercise319Sum
LeanPool.DomainTheory.Neighborhood.Exercise321
LeanPool.DomainTheory.Neighborhood.Exercise322
LeanPool.DomainTheory.Neighborhood.Exercise323
LeanPool.DomainTheory.Neighborhood.Exercise324
LeanPool.DomainTheory.Neighborhood.Exercise324Distrib
LeanPool.DomainTheory.Neighborhood.Exercise324Iter
LeanPool.DomainTheory.Neighborhood.Exercise325
LeanPool.DomainTheory.Neighborhood.Exercise326
LeanPool.DomainTheory.Neighborhood.Exercise326Sum
LeanPool.DomainTheory.Neighborhood.Exercise327
LeanPool.DomainTheory.Neighborhood.Exercise328
LeanPool.DomainTheory.Neighborhood.Exercise407
LeanPool.DomainTheory.Neighborhood.Exercise408
LeanPool.DomainTheory.Neighborhood.Exercise409
LeanPool.DomainTheory.Neighborhood.Exercise410
LeanPool.DomainTheory.Neighborhood.Exercise411
LeanPool.DomainTheory.Neighborhood.Exercise412
LeanPool.DomainTheory.Neighborhood.Exercise413
LeanPool.DomainTheory.Neighborhood.Exercise414
LeanPool.DomainTheory.Neighborhood.Exercise415
LeanPool.DomainTheory.Neighborhood.Exercise416
LeanPool.DomainTheory.Neighborhood.Exercise417
LeanPool.DomainTheory.Neighborhood.Exercise418
LeanPool.DomainTheory.Neighborhood.Exercise419
LeanPool.DomainTheory.Neighborhood.Exercise420
LeanPool.DomainTheory.Neighborhood.Exercise421
LeanPool.DomainTheory.Neighborhood.Exercise422
LeanPool.DomainTheory.Neighborhood.Exercise423
LeanPool.DomainTheory.Neighborhood.Exercise424
LeanPool.DomainTheory.Neighborhood.Exercise425
LeanPool.DomainTheory.Neighborhood.Exercise507
LeanPool.DomainTheory.Neighborhood.Exercise508
LeanPool.DomainTheory.Neighborhood.Exercise509
LeanPool.DomainTheory.Neighborhood.Exercise510
LeanPool.DomainTheory.Neighborhood.Exercise511
LeanPool.DomainTheory.Neighborhood.Exercise512
LeanPool.DomainTheory.Neighborhood.Exercise513
LeanPool.DomainTheory.Neighborhood.Exercise514
LeanPool.DomainTheory.Neighborhood.Exercise515
LeanPool.DomainTheory.Neighborhood.Exercise516
LeanPool.DomainTheory.Neighborhood.Exercise516Overlap
LeanPool.DomainTheory.Neighborhood.Exercise516ThueMorse
LeanPool.DomainTheory.Neighborhood.Exercise617
LeanPool.DomainTheory.Neighborhood.Exercise617Gen
LeanPool.DomainTheory.Neighborhood.Exercise618
LeanPool.DomainTheory.Neighborhood.Exercise619
LeanPool.DomainTheory.Neighborhood.Exercise619PartB
LeanPool.DomainTheory.Neighborhood.Exercise621
LeanPool.DomainTheory.Neighborhood.Exercise622
LeanPool.DomainTheory.Neighborhood.Exercise623
LeanPool.DomainTheory.Neighborhood.Exercise624
LeanPool.DomainTheory.Neighborhood.Exercise625
LeanPool.DomainTheory.Neighborhood.Exercise626
LeanPool.DomainTheory.Neighborhood.Exercise627
LeanPool.DomainTheory.Neighborhood.Exercise628
LeanPool.DomainTheory.Neighborhood.Exercise629
LeanPool.DomainTheory.Neighborhood.FunctionSpace
LeanPool.DomainTheory.Neighborhood.Lemma615
LeanPool.DomainTheory.Neighborhood.Product
LeanPool.DomainTheory.Neighborhood.Proposition53
LeanPool.DomainTheory.Neighborhood.Proposition54
LeanPool.DomainTheory.Neighborhood.Proposition611
LeanPool.DomainTheory.Neighborhood.Proposition612
LeanPool.DomainTheory.Neighborhood.Proposition66
LeanPool.DomainTheory.Neighborhood.Proposition67
LeanPool.DomainTheory.Neighborhood.Proposition77
LeanPool.DomainTheory.Neighborhood.Recursive
LeanPool.DomainTheory.Neighborhood.Table55
LeanPool.DomainTheory.Neighborhood.Theorem110
LeanPool.DomainTheory.Neighborhood.Theorem111
LeanPool.DomainTheory.Neighborhood.Theorem41
LeanPool.DomainTheory.Neighborhood.Theorem46
LeanPool.DomainTheory.Neighborhood.Theorem51
LeanPool.DomainTheory.Neighborhood.Theorem52
LeanPool.DomainTheory.Neighborhood.Theorem56
LeanPool.DomainTheory.Neighborhood.Theorem56Full
LeanPool.DomainTheory.Neighborhood.Theorem614
LeanPool.DomainTheory.Neighborhood.Theorem616
LeanPool.DomainTheory.Neighborhood.Theorem69
LeanPool.DomainTheory.Neighborhood.Theorem74
LeanPool.DomainTheory.Neighborhood.Theorem75
LeanPool.DomainTheory.Neighborhood.Theorem76
LeanPool.EcTateLean.FieldTheory.PerfectClosure
LeanPool.ErdosTuzaValtr.Config.Default
LeanPool.ErdosTuzaValtr.Config.Defs
LeanPool.ErdosTuzaValtr.Config.Lemmas
LeanPool.ErdosTuzaValtr.Config.Mirror
LeanPool.ErdosTuzaValtr.Etv.AlphaBeta
LeanPool.ErdosTuzaValtr.Etv.Default
LeanPool.ErdosTuzaValtr.Etv.Defs
LeanPool.ErdosTuzaValtr.Etv.Label
LeanPool.ErdosTuzaValtr.Etv.Mirror
LeanPool.ErdosTuzaValtr.Main.CapCup
LeanPool.ErdosTuzaValtr.Main.Defs
LeanPool.ErdosTuzaValtr.Main.InductionStep
LeanPool.ErdosTuzaValtr.Main.Main
LeanPool.FormalLearningTheory.Complexity.Amalgamation
LeanPool.FormalLearningTheory.Complexity.BorelAnalyticBridge
LeanPool.FormalLearningTheory.Complexity.Compression
LeanPool.FormalLearningTheory.Complexity.DualVC
LeanPool.FormalLearningTheory.Complexity.FiniteSupportUC
LeanPool.FormalLearningTheory.Complexity.GameInfra
LeanPool.FormalLearningTheory.Complexity.Generalization
LeanPool.FormalLearningTheory.Complexity.GeneralizationResults
LeanPool.FormalLearningTheory.Complexity.Interpolation
LeanPool.FormalLearningTheory.Complexity.Littlestone
LeanPool.FormalLearningTheory.Complexity.Measurability
LeanPool.FormalLearningTheory.Complexity.MindChange
LeanPool.FormalLearningTheory.Complexity.Ordinal
LeanPool.FormalLearningTheory.Complexity.Rademacher
LeanPool.FormalLearningTheory.Complexity.Structures
LeanPool.FormalLearningTheory.Complexity.Symmetrization
LeanPool.FormalLearningTheory.Complexity.VCDimension
LeanPool.FormalLearningTheory.Criterion.Extended
LeanPool.FormalLearningTheory.Criterion.Gold
LeanPool.FormalLearningTheory.Criterion.Online
LeanPool.FormalLearningTheory.Criterion.PAC
LeanPool.FormalLearningTheory.Learner.Active
LeanPool.FormalLearningTheory.Learner.Bayesian
LeanPool.FormalLearningTheory.Learner.Closure
LeanPool.FormalLearningTheory.Learner.Core
LeanPool.FormalLearningTheory.Learner.Monad
LeanPool.FormalLearningTheory.Learner.Properties
LeanPool.FormalLearningTheory.Learner.VersionSpace
LeanPool.FormalLearningTheory.PureMath.AnalyticMeasurability
LeanPool.FormalLearningTheory.PureMath.ApproxMinimax
LeanPool.FormalLearningTheory.PureMath.BinaryMatrix
LeanPool.FormalLearningTheory.PureMath.ChoquetCapacity
LeanPool.FormalLearningTheory.PureMath.Concentration
LeanPool.FormalLearningTheory.PureMath.Exchangeability
LeanPool.FormalLearningTheory.PureMath.FiniteVCApprox
LeanPool.FormalLearningTheory.PureMath.KLDivergence
LeanPool.FormalLearningTheory.PureMath.ReaderMonad
LeanPool.FormalLearningTheory.Theorem.BorelAnalyticSeparation
LeanPool.FormalLearningTheory.Theorem.Extended
LeanPool.FormalLearningTheory.Theorem.Gold
LeanPool.FormalLearningTheory.Theorem.Online
LeanPool.FormalLearningTheory.Theorem.PAC
LeanPool.FormalLearningTheory.Theorem.PACBayes
LeanPool.FormalLearningTheory.Theorem.Separation
LeanPool.FrontierMathOpenHypergraphs.Uniform.FrameBoosters
LeanPool.FrontierMathOpenHypergraphs.Uniform.FrameDefs
LeanPool.FrontierMathOpenHypergraphs.Uniform.FrameExact
LeanPool.FrontierMathOpenHypergraphs.Uniform.FrameResidues
LeanPool.FrontierMathOpenHypergraphs.Uniform.Frames
LeanPool.Incompleteness.Arith.D1
LeanPool.Incompleteness.Arith.D3
LeanPool.Incompleteness.Arith.DC
LeanPool.Incompleteness.Arith.First
LeanPool.Incompleteness.Arith.FormalizedArithmetic
LeanPool.Incompleteness.Arith.Second
LeanPool.Incompleteness.Arith.Theory
LeanPool.Incompleteness.DC.Basic
LeanPool.Incompleteness.ProvabilityLogic.Basic
LeanPool.Incompleteness.ToFoundation.Basic
LeanPool.Lean4GlCoalgebras.General.Completeness
LeanPool.Lean4GlCoalgebras.General.Game
LeanPool.Lean4GlCoalgebras.General.Proof
LeanPool.Lean4GlCoalgebras.General.Soundness
LeanPool.Lean4GlCoalgebras.Interpolation.Interpolants
LeanPool.Lean4GlCoalgebras.Interpolation.Interpolation
LeanPool.Lean4GlCoalgebras.Interpolation.PartialInterpolation
LeanPool.Lean4GlCoalgebras.Logic.FixedPointTheorem
LeanPool.Lean4GlCoalgebras.Logic.Semantics
LeanPool.Lean4GlCoalgebras.Logic.Syntax
LeanPool.Lean4GlCoalgebras.Pdl.Game
LeanPool.Lean4GlCoalgebras.Split.Completeness
LeanPool.Lean4GlCoalgebras.Split.CutProof
LeanPool.Lean4GlCoalgebras.Split.Game
LeanPool.Lean4GlCoalgebras.Split.Proof
LeanPool.Lean4GlCoalgebras.Split.ProofTransformations
LeanPool.Lean4GlCoalgebras.Split.Soundness
LeanPool.Lean4Itree.ITree.Basic
LeanPool.Lean4Itree.ITree.EffectAlgebra
LeanPool.Lean4Itree.ITree.Monad
LeanPool.Lean4Itree.ITree.Utils
LeanPool.Lean4Itree.Paco.Paco
LeanPool.Lean4Itree.Paco.PacoDefs
LeanPool.Lean4Itree.Paco.PacoTactics
LeanPool.LeanBooleanfun.ToMathlib.Finset
LeanPool.LeanComplexAnalysis.Harmonic.PoissonIntegral
LeanPool.LeanComplexAnalysis.Harmonic.PoissonIntegral2
LeanPool.LeanComplexAnalysis.Harmonic.PoissonIntegralCircleAverage
LeanPool.LeanComplexAnalysis.Harmonic.Positive
LeanPool.LeanComplexAnalysis.UnivalentFunctions.ClassS
LeanPool.LeanModularForms.ContourIntegral.CrossingLimit
LeanPool.LeanModularForms.ContourIntegral.PVSplit
LeanPool.LeanModularForms.ContourIntegral.SegmentFTC
LeanPool.LeanModularForms.ContourIntegral.WindingNumber
LeanPool.LeanModularForms.ForMathlib.AtImInfty
LeanPool.LeanModularForms.ForMathlib.Bounds
LeanPool.LeanModularForms.ForMathlib.CongruenceSubgroupsCopy
LeanPool.LeanModularForms.ForMathlib.CongruenceSubgrps
LeanPool.LeanModularForms.ForMathlib.FunctionsBoundedAtInfty
LeanPool.LeanModularForms.ForMathlib.Hassumunifon
LeanPool.LeanModularForms.ForMathlib.Identities
LeanPool.LeanModularForms.ForMathlib.Instances
LeanPool.LeanModularForms.ForMathlib.IsBoundedAtImInfty
LeanPool.LeanModularForms.ForMathlib.LevelOne
LeanPool.LeanModularForms.ForMathlib.Petersson
LeanPool.LeanModularForms.ForMathlib.QExpansion
LeanPool.LeanModularForms.ForMathlib.SlashActions
LeanPool.LeanModularForms.ForMathlib.UpperHalfPlane
LeanPool.LeanModularForms.GeneralizedResidueTheory.ArcCalculus
LeanPool.LeanModularForms.GeneralizedResidueTheory.Basic
LeanPool.LeanModularForms.GeneralizedResidueTheory.Bridges
LeanPool.LeanModularForms.GeneralizedResidueTheory.CauchyPrimitive
LeanPool.LeanModularForms.GeneralizedResidueTheory.CurveAvoidance
LeanPool.LeanModularForms.GeneralizedResidueTheory.Cycle
LeanPool.LeanModularForms.GeneralizedResidueTheory.GeneralizedResidueTheorem
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy
LeanPool.LeanModularForms.GeneralizedResidueTheory.LogDerivFTC
LeanPool.LeanModularForms.GeneralizedResidueTheory.PiecewiseCurveAPI
LeanPool.LeanModularForms.GeneralizedResidueTheory.PrincipalValue
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing
LeanPool.LeanModularForms.Modularforms.AtImInfty
LeanPool.LeanModularForms.Modularforms.BigO
LeanPool.LeanModularForms.Modularforms.Cauchylems
LeanPool.LeanModularForms.Modularforms.ClogArgLems
LeanPool.LeanModularForms.Modularforms.Cotangent
LeanPool.LeanModularForms.Modularforms.Csqrt
LeanPool.LeanModularForms.Modularforms.Delta
LeanPool.LeanModularForms.Modularforms.Derivative
LeanPool.LeanModularForms.Modularforms.DimensionFormulas
LeanPool.LeanModularForms.Modularforms.E2
LeanPool.LeanModularForms.Modularforms.Eisenstein
LeanPool.LeanModularForms.Modularforms.EisensteinAsymptotics
LeanPool.LeanModularForms.Modularforms.Eisensteinqexpansions
LeanPool.LeanModularForms.Modularforms.Equivs
LeanPool.LeanModularForms.Modularforms.Eta
LeanPool.LeanModularForms.Modularforms.EtaCleanup
LeanPool.LeanModularForms.Modularforms.ExpLems
LeanPool.LeanModularForms.Modularforms.ForMathlibCusps
LeanPool.LeanModularForms.Modularforms.ForMathlibFunctionsBoundedAtInfty
LeanPool.LeanModularForms.Modularforms.ForMathlibSlashActions
LeanPool.LeanModularForms.Modularforms.ForMathlibUpperHalfPlane
LeanPool.LeanModularForms.Modularforms.Generators
LeanPool.LeanModularForms.Modularforms.IccIcoLems
LeanPool.LeanModularForms.Modularforms.IsCuspForm
LeanPool.LeanModularForms.Modularforms.Iteratedderivs
LeanPool.LeanModularForms.Modularforms.JacobiTheta
LeanPool.LeanModularForms.Modularforms.LimunderLems
LeanPool.LeanModularForms.Modularforms.LogDerivLems
LeanPool.LeanModularForms.Modularforms.MDifferentiableFunProp
LeanPool.LeanModularForms.Modularforms.MultipliableLems
LeanPool.LeanModularForms.Modularforms.PhiTransform
LeanPool.LeanModularForms.Modularforms.QExpansion
LeanPool.LeanModularForms.Modularforms.QExpansionLems
LeanPool.LeanModularForms.Modularforms.RamanujanIdentities
LeanPool.LeanModularForms.Modularforms.ResToImagAxis
LeanPool.LeanModularForms.Modularforms.RiemannZetalems
LeanPool.LeanModularForms.Modularforms.SerreDerivativeSlash
LeanPool.LeanModularForms.Modularforms.SlashActionAuxil
LeanPool.LeanModularForms.Modularforms.SummableLems
LeanPool.LeanModularForms.Modularforms.Tendstolems
LeanPool.LeanModularForms.Modularforms.ThetaDerivIdentities
LeanPool.LeanModularForms.Modularforms.TsumderivWithin
LeanPool.LeanModularForms.Modularforms.Uniformcts
LeanPool.LeanModularForms.Modularforms.Upperhalfplane
LeanPool.LeanModularForms.SpherePacking.CuspDecay
LeanPool.LeanModularForms.SpherePacking.PhiHolomorphic
LeanPool.LeanModularForms.SpherePacking.ViazovskaMagicFunction
LeanPool.LeanModularForms.ValenceFormula.CoreIdentity
LeanPool.LeanModularForms.ValenceFormula.Definitions
LeanPool.LeanModularForms.ValenceFormula.InteriorWinding
LeanPool.LeanModularForms.ValenceFormula.ModularInvariance
LeanPool.LeanModularForms.ValenceFormula.OrbitPairing
LeanPool.LeanModularForms.ValenceFormula.OrbitSum
LeanPool.LeanModularForms.ValenceFormula.PVChain
LeanPool.LeanModularForms.ValenceFormula.TextbookExistence
LeanPool.LeanModularForms.ValenceFormula.TextbookForm
LeanPool.LeanModularForms.ValenceFormula.TrigLemmas
LeanPool.LeanModularForms.ValenceFormula.WindingWeights
LeanPool.LeanPolyABC.Corollaries.Davenport
LeanPool.LeanPolyABC.Corollaries.FltCatalan
LeanPool.LeanPolyABC.Corollaries.NoParametrization
LeanPool.LeanPolyABC.Lib.DivRadical
LeanPool.LeanPolyABC.Lib.Max3
LeanPool.LeanPolyABC.Lib.Radical
LeanPool.LeanPolyABC.Lib.Wronskian
LeanPool.LeanQuantumAlg.Algorithms.AmplitudeEstimation
LeanPool.LeanQuantumAlg.Algorithms.BernsteinVazirani
LeanPool.LeanQuantumAlg.Algorithms.DeutschJozsa
LeanPool.LeanQuantumAlg.Algorithms.GHZ
LeanPool.LeanQuantumAlg.Algorithms.Grover
LeanPool.LeanQuantumAlg.Algorithms.OrderFinding
LeanPool.LeanQuantumAlg.Algorithms.QPE
LeanPool.LeanQuantumAlg.Algorithms.Simon
LeanPool.LeanQuantumAlg.Algorithms.SuperdenseCoding
LeanPool.LeanQuantumAlg.Algorithms.Teleportation
LeanPool.LeanQuantumAlg.Core.Components
LeanPool.LeanQuantumAlg.Core.Cost
LeanPool.LeanQuantumAlg.Core.Gate
LeanPool.LeanQuantumAlg.Core.Measurement
LeanPool.LeanQuantumAlg.Core.State
LeanPool.LeanQuantumAlg.Core.Tensor
LeanPool.LeanQuantumAlg.Primitives.AmplitudeAmplification
LeanPool.LeanQuantumAlg.Primitives.BellPair
LeanPool.LeanQuantumAlg.Primitives.ControlledTransform
LeanPool.LeanQuantumAlg.Primitives.HadamardTest
LeanPool.LeanQuantumAlg.Primitives.LCU
LeanPool.LeanQuantumAlg.Primitives.ParameterShift
LeanPool.LeanQuantumAlg.Primitives.PhaseKickback
LeanPool.LeanQuantumAlg.Primitives.QFT
LeanPool.LeanQuantumAlg.Primitives.QKernel
LeanPool.LeanQuantumAlg.Primitives.QNN
LeanPool.LeanQuantumAlg.Primitives.QSP
LeanPool.LeanQuantumAlg.Primitives.SwapTest
LeanPool.LeanQuantumAlg.Primitives.WalshHadamard
LeanPool.LeanQuantumAlg.Util.Complex
LeanPool.LeanQuantumAlg.Util.Concentration
LeanPool.LeanQuantumAlg.Util.FinPow
LeanPool.LeanQuantumAlg.Util.HilbertSchmidt
LeanPool.LeanQuantumAlg.Util.Polynomial
LeanPool.LeanQuantumAlg.Util.TrigPolynomial
LeanPool.Lentil.Gadgets.TheoremDeriving
LeanPool.Lentil.Gadgets.TheoremLifting
LeanPool.Lentil.ProofMode.Basic
LeanPool.Lentil.ProofMode.Display
LeanPool.Lentil.ProofMode.Location
LeanPool.Lentil.ProofMode.Tactics
LeanPool.Lentil.Rules.Basic
LeanPool.Lentil.Rules.BigOp
LeanPool.Lentil.Rules.LeadsTo
LeanPool.Lentil.Rules.StatePred
LeanPool.Lentil.Rules.WF
LeanPool.Lentil.Tactics.Basic
LeanPool.Lentil.Tactics.FiniteWindow
LeanPool.Lentil.Utils.MetaUtil
LeanPool.Lentil.Utils.MiscLemmas
LeanPool.Lentil.Utils.SyntaxUtil
LeanPool.MRiscX.AbstractSyntax.AbstractSyntax
LeanPool.MRiscX.AbstractSyntax.Instr
LeanPool.MRiscX.AbstractSyntax.MState
LeanPool.MRiscX.AbstractSyntax.Map
LeanPool.MRiscX.Delab.DelabCode
LeanPool.MRiscX.Delab.DelabHoare
LeanPool.MRiscX.Elab.CodeElaborator
LeanPool.MRiscX.Elab.HandleExpr
LeanPool.MRiscX.Elab.HandleNumOrIdent
LeanPool.MRiscX.Elab.HoareElaborator
LeanPool.MRiscX.Examples.Examples
LeanPool.MRiscX.Examples.OtpProof
LeanPool.MRiscX.Examples.SingleProofsOTP
LeanPool.MRiscX.Examples.SpecAutomation
LeanPool.MRiscX.Hoare.EvalLabelInHoare
LeanPool.MRiscX.Hoare.HoareAssignmentElab
LeanPool.MRiscX.Hoare.HoareCore
LeanPool.MRiscX.Hoare.HoareRules
LeanPool.MRiscX.Hoare.HoareTheory
LeanPool.MRiscX.Parser.AssemblySyntax
LeanPool.MRiscX.Parser.HoareSyntax
LeanPool.MRiscX.Semantics.MsTheory
LeanPool.MRiscX.Semantics.Run
LeanPool.MRiscX.Semantics.Specification
LeanPool.MRiscX.Tactics.ApplySpec
LeanPool.MRiscX.Tactics.CodeProofTactics
LeanPool.MRiscX.Tactics.GeneralCustomTactics
LeanPool.MRiscX.Tactics.HelpCodeProofTactics
LeanPool.MRiscX.Tactics.SpecificationTactics
LeanPool.MRiscX.Tactics.SplitLastSeq
LeanPool.MRiscX.Tactics.TacticUtil
LeanPool.MRiscX.Util.BasicTheorems
LeanPool.MisereGames.AugmentedForm.Lift
LeanPool.MisereGames.AugmentedForm.Short
LeanPool.MisereGames.Form.Adjoint
LeanPool.MisereGames.Form.Birthday
LeanPool.MisereGames.Form.Classes
LeanPool.MisereGames.Form.Short
LeanPool.MisereGames.GameForm.Birthday
LeanPool.MisereGames.GameForm.Special
LeanPool.MisereGames.Literature.OnSumsOfPFreeFormsUnderMiserePlay
LeanPool.MisereGames.Mathlib.NatOrdinal
LeanPool.MisereGames.Mathlib.SimpleGraph
LeanPool.MisereGames.Mathlib.Small
LeanPool.MisereGames.Misere.Ambient
LeanPool.MisereGames.Misere.Blocking
LeanPool.MisereGames.Misere.Closures
LeanPool.MisereGames.Misere.Comparison
LeanPool.MisereGames.Misere.DeadEnding
LeanPool.MisereGames.Misere.IntegerInvertible
LeanPool.MisereGames.Misere.LiftIncomparable
LeanPool.MisereGames.Misere.NonInvertible
LeanPool.MisereGames.Misere.Normal
LeanPool.MisereGames.Misere.OutcomeStable
LeanPool.MisereGames.Misere.PFree
LeanPool.MisereGames.Misere.PFreeBlocking
LeanPool.MisereGames.Misere.PFreeDeadEnding
LeanPool.MisereGames.Misere.Preservation
LeanPool.MisereGames.Misere.Quotients
LeanPool.MisereGames.Misere.Separation
LeanPool.MisereGames.Misere.ShortIncomparable
LeanPool.MisereGames.Misere.Stride
LeanPool.MisereGames.Misere.TippingPoints
LeanPool.MisereGames.Misere.Universe
LeanPool.MisereGames.Ruleset.Hackenbush
LeanPool.MisereGames.Ruleset.Push
LeanPool.MisereGames.Ruleset.Shove
LeanPool.MisereGames.Ruleset.Strip
LeanPool.MisereGames.Tactic.DocAlias
LeanPool.Monlib4.LinearAlgebra.Coalgebra
LeanPool.Monlib4.LinearAlgebra.DirectSumFromTo
LeanPool.Monlib4.LinearAlgebra.End
LeanPool.Monlib4.LinearAlgebra.InnerAut
LeanPool.Monlib4.LinearAlgebra.InvariantSubmodule
LeanPool.Monlib4.LinearAlgebra.Ips
LeanPool.Monlib4.LinearAlgebra.IsProjPrime
LeanPool.Monlib4.LinearAlgebra.IsReal
LeanPool.Monlib4.LinearAlgebra.KroneckerToTensor
LeanPool.Monlib4.LinearAlgebra.LinearMapOp
LeanPool.Monlib4.LinearAlgebra.LmulRmul
LeanPool.Monlib4.LinearAlgebra.Matrix
LeanPool.Monlib4.LinearAlgebra.MulPrimePrime
LeanPool.Monlib4.LinearAlgebra.MyBimodule
LeanPool.Monlib4.LinearAlgebra.MySpec
LeanPool.Monlib4.LinearAlgebra.Nacgor
LeanPool.Monlib4.LinearAlgebra.OfNorm
LeanPool.Monlib4.LinearAlgebra.PiDirectSum
LeanPool.Monlib4.LinearAlgebra.PiStarOrderedRing
LeanPool.Monlib4.LinearAlgebra.PosMapIsReal
LeanPool.Monlib4.LinearAlgebra.QuantumSet
LeanPool.Monlib4.LinearAlgebra.TensorProduct
LeanPool.Monlib4.LinearAlgebra.ToMatrixOfEquiv
LeanPool.Monlib4.Other.Sonia
LeanPool.Monlib4.Preq.Complex
LeanPool.Monlib4.Preq.Dite
LeanPool.Monlib4.Preq.Equiv
LeanPool.Monlib4.Preq.Finset
LeanPool.Monlib4.Preq.Ites
LeanPool.Monlib4.Preq.RCLikeLe
LeanPool.Monlib4.Preq.Set
LeanPool.Monlib4.Preq.StarAlgEquiv
LeanPool.Monlib4.QuantumGraph.Basic
LeanPool.Monlib4.QuantumGraph.Degree
LeanPool.Monlib4.QuantumGraph.Example
LeanPool.Monlib4.QuantumGraph.Grad
LeanPool.Monlib4.QuantumGraph.Iso
LeanPool.Monlib4.QuantumGraph.Matrix
LeanPool.Monlib4.QuantumGraph.Nontracial
LeanPool.Monlib4.QuantumGraph.OfClassicalGraph
LeanPool.Monlib4.QuantumGraph.PiMat
LeanPool.Monlib4.QuantumGraph.PiMatFinTwo
LeanPool.Monlib4.QuantumGraph.QamA
LeanPool.Monlib4.QuantumGraph.QamAExample
LeanPool.Monlib4.QuantumGraph.ToProjections
LeanPool.Monlib4.RepTheory.AutMat
LeanPool.OSforGFF.Bochner.FejerPD
LeanPool.OSforGFF.Bochner.Main
LeanPool.OSforGFF.Bochner.PositiveDefinite
LeanPool.OSforGFF.Bochner.Sazonov
LeanPool.OSforGFF.Covariance.Momentum
LeanPool.OSforGFF.Covariance.Parseval
LeanPool.OSforGFF.Covariance.Position
LeanPool.OSforGFF.Covariance.RealForm
LeanPool.OSforGFF.GaussianField.Nuclear
LeanPool.OSforGFF.GaussianField.SchwartzNuclear
LeanPool.OSforGFF.General.BesselFunction
LeanPool.OSforGFF.General.FourierTransforms
LeanPool.OSforGFF.General.FrobeniusPositivity
LeanPool.OSforGFF.General.FunctionalAnalysis
LeanPool.OSforGFF.General.GaussianRBF
LeanPool.OSforGFF.General.HadamardExp
LeanPool.OSforGFF.General.L2TimeIntegral
LeanPool.OSforGFF.General.LaplaceIntegral
LeanPool.OSforGFF.General.PositiveDefinite
LeanPool.OSforGFF.General.QuantitativeDecay
LeanPool.OSforGFF.General.SchurProduct
LeanPool.OSforGFF.General.SchwartzTranslationDecay
LeanPool.OSforGFF.KolmogorovExtension4.AuxLemmas
LeanPool.OSforGFF.KolmogorovExtension4.CompactSystem
LeanPool.OSforGFF.KolmogorovExtension4.KolmogorovExtension
LeanPool.OSforGFF.KolmogorovExtension4.RegularContent
LeanPool.OSforGFF.KolmogorovExtension4.Semiring
LeanPool.OSforGFF.Measure.Construct
LeanPool.OSforGFF.Measure.GaussianFreeField
LeanPool.OSforGFF.Measure.IsGaussian
LeanPool.OSforGFF.Measure.Minlos
LeanPool.OSforGFF.Measure.MinlosAnalytic
LeanPool.OSforGFF.Measure.NuclearSpace
LeanPool.OSforGFF.Minlos.FinDimMarginals
LeanPool.OSforGFF.Minlos.Main
LeanPool.OSforGFF.Minlos.MeasurableModification
LeanPool.OSforGFF.Minlos.MinlosConcentration
LeanPool.OSforGFF.Minlos.NuclearSpace
LeanPool.OSforGFF.Minlos.PietschBridge
LeanPool.OSforGFF.Minlos.ProjectiveFamily
LeanPool.OSforGFF.Minlos.SazonovTightness
LeanPool.OSforGFF.OS.Axioms
LeanPool.OSforGFF.OS.Master
LeanPool.OSforGFF.OS.NonTrivial
LeanPool.OSforGFF.OS.OS0Analyticity
LeanPool.OSforGFF.OS.OS1Regularity
LeanPool.OSforGFF.OS.OS2Invariance
LeanPool.OSforGFF.OS.OS3CovarianceRP
LeanPool.OSforGFF.OS.OS3MixedRep
LeanPool.OSforGFF.OS.OS3MixedRepInfra
LeanPool.OSforGFF.OS.OS3ReflectionPositivity
LeanPool.OSforGFF.OS.OS4Clustering
LeanPool.OSforGFF.OS.OS4Ergodicity
LeanPool.OSforGFF.OS.OS4MGF
LeanPool.OSforGFF.Schwinger.Defs
LeanPool.OSforGFF.Schwinger.GaussianMoments
LeanPool.OSforGFF.Schwinger.TwoPoint
LeanPool.OSforGFF.Spacetime.Basic
LeanPool.OSforGFF.Spacetime.ComplexTestFunction
LeanPool.OSforGFF.Spacetime.Decomposition
LeanPool.OSforGFF.Spacetime.DiscreteSymmetry
LeanPool.OSforGFF.Spacetime.Euclidean
LeanPool.OSforGFF.Spacetime.PositiveTimeTestFunction
LeanPool.OSforGFF.Spacetime.ProdIntegrable
LeanPool.OSforGFF.Spacetime.TimeTranslation
LeanPool.OSforGFF.Spacetime.Tonelli
LeanPool.PCFTheory.Background.Club
LeanPool.PCFTheory.Background.Cofinality
LeanPool.PCFTheory.Background.Ordinal
LeanPool.PCFTheory.Background.Topology
LeanPool.PLAcceleratedNesterovLean.Convergence.Bootstrap
LeanPool.PLAcceleratedNesterovLean.Convergence.Coercivity
LeanPool.PLAcceleratedNesterovLean.Convergence.ConvergenceHelpers
LeanPool.PLAcceleratedNesterovLean.Convergence.CurvAbsorb
LeanPool.PLAcceleratedNesterovLean.Convergence.GenLocalArgument
LeanPool.PLAcceleratedNesterovLean.Convergence.LocalArgument
LeanPool.PLAcceleratedNesterovLean.Convergence.LocalGeometry
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction
LeanPool.PLAcceleratedNesterovLean.Convergence.MainTheoremInternal
LeanPool.PLAcceleratedNesterovLean.Convergence.MotionError
LeanPool.PLAcceleratedNesterovLean.Convergence.NesterovConvergence
LeanPool.PLAcceleratedNesterovLean.Convergence.PhaseSchedule
LeanPool.PLAcceleratedNesterovLean.Convergence.RateArithmetic
LeanPool.PLAcceleratedNesterovLean.Convergence.StateContraction
LeanPool.PLAcceleratedNesterovLean.Core.Defs
LeanPool.PLAcceleratedNesterovLean.Core.EmbeddedManifold
LeanPool.PLAcceleratedNesterovLean.Core.NesterovScheme
LeanPool.PLAcceleratedNesterovLean.Core.NesterovSeqGen
LeanPool.PLAcceleratedNesterovLean.MorseBott.Bridge
LeanPool.PLAcceleratedNesterovLean.MorseBott.BridgeDefs
LeanPool.PLAcceleratedNesterovLean.MorseBott.Defs
LeanPool.PLAcceleratedNesterovLean.MorseBott.GradAlign
LeanPool.PLAcceleratedNesterovLean.MorseBott.HessianPL
LeanPool.PLAcceleratedNesterovLean.MorseBott.IFTProof
LeanPool.PLAcceleratedNesterovLean.MorseBott.NormalHessianBound
LeanPool.PLAcceleratedNesterovLean.MorseBott.PLImpliesMB
LeanPool.PLAcceleratedNesterovLean.MorseBott.Submanifold
LeanPool.PLAcceleratedNesterovLean.MorseBott.TubularProjection
LeanPool.Polylean.Complexes.GraphPaths
LeanPool.Polylean.ConjInvLength.Length
LeanPool.Polylean.ConjInvLength.LengthBound
LeanPool.Polylean.ConjInvLength.LengthNode
LeanPool.Polylean.ConjInvLength.MemoLength
LeanPool.Polylean.ConjInvLength.ProvedBound
LeanPool.Polylean.ConjInvLength.WordTree
LeanPool.Polylean.UnitConjecture.AddFreeGroup
LeanPool.Polylean.UnitConjecture.Cocycle
LeanPool.Polylean.UnitConjecture.EnumDecide
LeanPool.Polylean.UnitConjecture.FreeModule
LeanPool.Polylean.UnitConjecture.GardamGroup
LeanPool.Polylean.UnitConjecture.GardamTheorem
LeanPool.Polylean.UnitConjecture.GroupRing
LeanPool.Polylean.UnitConjecture.MetabelianGroup
LeanPool.Polylean.UnitConjecture.Tactics
LeanPool.Polylean.UnitConjecture.TorsionFree
LeanPool.PumpingCfg.ChomskyNormalForm.Basic
LeanPool.PumpingCfg.ChomskyNormalForm.ContextFreeGrammarExtras
LeanPool.PumpingCfg.ChomskyNormalForm.EmptyElimination
LeanPool.PumpingCfg.ChomskyNormalForm.LengthRestriction
LeanPool.PumpingCfg.ChomskyNormalForm.TerminalRestriction
LeanPool.PumpingCfg.ChomskyNormalForm.Translation
LeanPool.PumpingCfg.ChomskyNormalForm.UnitElimination
LeanPool.QuasiBorelSpaces.List.Encoding
LeanPool.QuasiBorelSpaces.MeasureTheory.Cases
LeanPool.QuasiBorelSpaces.MeasureTheory.Instances
LeanPool.QuasiBorelSpaces.MeasureTheory.List
LeanPool.QuasiBorelSpaces.MeasureTheory.Measure
LeanPool.QuasiBorelSpaces.MeasureTheory.Option
LeanPool.QuasiBorelSpaces.MeasureTheory.Pack
LeanPool.QuasiBorelSpaces.MeasureTheory.ProbabilityMeasure
LeanPool.QuasiBorelSpaces.MeasureTheory.Quantile
LeanPool.QuasiBorelSpaces.MeasureTheory.Randomization
LeanPool.QuasiBorelSpaces.MeasureTheory.Sigma
LeanPool.QuasiBorelSpaces.MeasureTheory.StandardBorelSpace
LeanPool.QuasiBorelSpaces.MeasureTheory.Sum
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Basic
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Fix
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Option
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Sigma
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Sum
LeanPool.QuasiBorelSpaces.Option.Instances
LeanPool.QuasiBorelSpaces.Rose.Encoding
LeanPool.QuasiBorelSpaces.RoseTree.Basic
LeanPool.QuasiBorelSpaces.RoseTree.Defs
LeanPool.QuasiBorelSpaces.UnitInterval.AssocProd
LeanPool.Redhill.Common.Conjectures
LeanPool.Redhill.Common.MaxAbs
LeanPool.Redhill.Common.PairwiseCoprime
LeanPool.Redhill.Common.PrimeChain
LeanPool.Redhill.Common.Quality
LeanPool.Redhill.Common.SubsumCondition
LeanPool.Redhill.Common.VWPair
LeanPool.Redhill.General.Coprime
LeanPool.Redhill.General.Defs
LeanPool.Redhill.General.Main
LeanPool.Redhill.General.Subsum
LeanPool.Redhill.Odd.Defs
LeanPool.Redhill.Odd.Main
LeanPool.Redhill.Odd.Pell
LeanPool.Redhill.Odd.Subsum
LeanPool.Redhill.ToMathlib.NatAbs
LeanPool.Redhill.ToMathlib.NatSumProd
LeanPool.RlTheoryInLean.Analysis.Normed
LeanPool.RlTheoryInLean.Data.Matrix
LeanPool.RlTheoryInLean.MeasureTheory.Function
LeanPool.RlTheoryInLean.MeasureTheory.MeasurableSpace
LeanPool.RlTheoryInLean.MeasureTheory.Measure
LeanPool.RlTheoryInLean.Order.Filter
LeanPool.RlTheoryInLean.Probability.Kernel
LeanPool.RlTheoryInLean.Probability.MarkovChain
LeanPool.RlTheoryInLean.StochasticApproximation.DiscreteGronwall
LeanPool.Rupert.Equivalences.AffineRupertEquivRupertSet
LeanPool.Rupert.Equivalences.RupertEquivRupertPrime
LeanPool.Rupert.Equivalences.RupertEquivRupertSet
LeanPool.Rupert.Equivalences.Util
LeanPool.SardMoreira.ToMathlib.ContinuousLinearMap
LeanPool.SardMoreira.ToMathlib.PR31960
LeanPool.SardMoreira.ToMathlib.PR32186
LeanPool.SardMoreira.ToMathlib.PR32986
LeanPool.SardMoreira.ToMathlib.PR32993
LeanPool.SardMoreira.ToMathlib.PR33029
LeanPool.SardMoreira.ToMathlib.PR33114
LeanPool.SelbergSieve4.Applications.BrunTitchmarsh
LeanPool.SelbergSieve4.Applications.PrimeCountingUpperBound
LeanPool.SelbergSieve4.ForMathlib.Basic
LeanPool.SelbergSieve4.ForMathlib.ProdsAntidiagonal
LeanPool.SelbergSieve4.Tactic.AesopDiv
LeanPool.SelbergSieve4.Tactic.AesopInit
LeanPool.SelbergSieve4.Tactic.Multiplicativity
LeanPool.Shannon1948Formalization.Entropy.Approx
LeanPool.Shannon1948Formalization.Entropy.Converse
LeanPool.Shannon1948Formalization.Entropy.Core
LeanPool.Shannon1948Formalization.Entropy.Final
LeanPool.Shannon1948Formalization.Entropy.Gibbs
LeanPool.Shannon1948Formalization.Entropy.Joint
LeanPool.Shannon1948Formalization.Entropy.Properties
LeanPool.Shannon1948Formalization.Entropy.Rational
LeanPool.Shannon1948Formalization.Entropy.Uniform
LeanPool.SingularModuli.QuadraticOrder.Basic
LeanPool.SingularModuli.QuadraticOrder.CanonicalForm
LeanPool.SingularModuli.QuadraticOrder.Discriminant
LeanPool.SingularModuli.QuadraticOrder.Norm
LeanPool.SingularModuli.QuadraticOrder.Prime
LeanPool.SingularModuli.QuadraticOrder.RootCounting
LeanPool.SingularModuli.QuadraticOrder.Verification
LeanPool.TwoColoringOneRound.LowerBound.Certificate
LeanPool.TwoColoringOneRound.LowerBound.CorrAvgMatrix
LeanPool.TwoColoringOneRound.LowerBound.Correlation
LeanPool.TwoColoringOneRound.LowerBound.Defs
LeanPool.TwoColoringOneRound.LowerBound.EdgePatterns
LeanPool.TwoColoringOneRound.LowerBound.LocalRule
LeanPool.TwoColoringOneRound.LowerBound.N1000000AvailFrom
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionCompute
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeBase
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0Int
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock0
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock1
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock2
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock4
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock5
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntBlock6
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeS0IntGoal
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSi
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiInt
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0Vars0to3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0Vars12to15
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0Vars16to19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0Vars20to22
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0Vars4to7
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock0Vars8to11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1Vars0to3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1Vars12to15
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1Vars16to19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1Vars20to22
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1Vars4to7
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock1Vars8to11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars0to3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars12to15
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars16to19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars20to22
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars4to7
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock2Vars8to11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3Vars0to3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3Vars12to15
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3Vars16to19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3Vars20to22
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3Vars4to7
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock3Vars8to11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars0to3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars12to15
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars16to19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars20to22
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars4to7
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock4Vars8to11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars0to3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars12to15
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars16to19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars20to22
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars4to7
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock5Vars8to11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars0to3
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars12to15
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars16to19
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars20to22
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars4to7
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntBlock6Vars8to11
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionComputeSiIntGoal
LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionForB
LeanPool.TwoColoringOneRound.LowerBound.N1000000Bound
LeanPool.TwoColoringOneRound.LowerBound.N1000000CorrAvgMatrixDecompose
LeanPool.TwoColoringOneRound.LowerBound.N1000000CorrAvgMatrixSymmDecompose
LeanPool.TwoColoringOneRound.LowerBound.N1000000Data
LeanPool.TwoColoringOneRound.LowerBound.N1000000Interface
LeanPool.TwoColoringOneRound.LowerBound.N1000000IntersectionCounting
LeanPool.TwoColoringOneRound.LowerBound.N1000000Main
LeanPool.TwoColoringOneRound.LowerBound.N1000000MaskAtFacts
LeanPool.TwoColoringOneRound.LowerBound.N1000000MaskComplete
LeanPool.TwoColoringOneRound.LowerBound.N1000000MuLinear
LeanPool.TwoColoringOneRound.LowerBound.N1000000MuWitness
LeanPool.TwoColoringOneRound.LowerBound.N1000000Objective
LeanPool.TwoColoringOneRound.LowerBound.N1000000OrbitCounting
LeanPool.TwoColoringOneRound.LowerBound.N1000000OrbitalBasis
LeanPool.TwoColoringOneRound.LowerBound.N1000000PairTransitivity
LeanPool.TwoColoringOneRound.LowerBound.N1000000Relaxation
LeanPool.TwoColoringOneRound.LowerBound.N1000000RelaxationPsdSoundness
LeanPool.TwoColoringOneRound.LowerBound.N1000000StructureConstants
LeanPool.TwoColoringOneRound.LowerBound.N1000000Transitivity
LeanPool.TwoColoringOneRound.LowerBound.N1000000WeakDuality
LeanPool.TwoColoringOneRound.LowerBound.N1000000WedderburnData
LeanPool.TwoColoringOneRound.LowerBound.N1000000Witness
LeanPool.TwoColoringOneRound.LowerBound.N1000000Z
LeanPool.TwoColoringOneRound.LowerBound.N1000000ZData
LeanPool.TwoColoringOneRound.LowerBound.N9
LeanPool.TwoColoringOneRound.LowerBound.OverlapType
LeanPool.TwoColoringOneRound.LowerBound.Sanity
LeanPool.TwoColoringOneRound.LowerBound.UpperBound
LeanPool.TwoColoringOneRound.UpperBound.Recursive3Param
LeanPool.VirasoroProject.ToMathlib.Algebra
LeanPool.VirasoroProject.ToMathlib.LinearAlgebra
LeanPool.VirasoroProject.ToMathlib.Topology
LeanPool.WhiteheadTheorem.CWComplex.Basic
LeanPool.WhiteheadTheorem.Compressible.CWComplex
LeanPool.WhiteheadTheorem.Compressible.Defs
LeanPool.WhiteheadTheorem.Compressible.Disk
LeanPool.WhiteheadTheorem.Compressible.WeakEquiv
LeanPool.WhiteheadTheorem.HEP.Cofibration
LeanPool.WhiteheadTheorem.HEP.Cube
LeanPool.WhiteheadTheorem.HEP.CubeJar
LeanPool.WhiteheadTheorem.HEP.Retract
LeanPool.WhiteheadTheorem.HomotopyGroup.ChangeBasePt
LeanPool.WhiteheadTheorem.HomotopyGroup.InducedMaps
LeanPool.WhiteheadTheorem.RelHomotopyGroup.Algebra
LeanPool.WhiteheadTheorem.RelHomotopyGroup.Compression
LeanPool.WhiteheadTheorem.RelHomotopyGroup.Defs
LeanPool.WhiteheadTheorem.RelHomotopyGroup.LongExactSeq
LeanPool.WhiteheadTheorem.Shapes.Cube
LeanPool.WhiteheadTheorem.Shapes.CubeBoundaryMap
LeanPool.WhiteheadTheorem.Shapes.Disk
LeanPool.WhiteheadTheorem.Shapes.DiskHomeoCube
LeanPool.WhiteheadTheorem.Shapes.Jar
LeanPool.WhiteheadTheorem.Shapes.MappingCylinder
LeanPool.WhiteheadTheorem.Shapes.Maps
LeanPool.WhiteheadTheorem.Shapes.Pushout
LeanPool.WhiteheadTheorem.Shapes.UnitInterval
LeanPool.ZhangYeungInequality.Test.CopyLemma
LeanPool.ZhangYeungInequality.Test.Delta
LeanPool.ZhangYeungInequality.Test.EntropyRegion
LeanPool.ZhangYeungInequality.Test.Theorem2
LeanPool.ZhangYeungInequality.Test.Theorem3
LeanPool.ZhangYeungInequality.Test.Theorem4
LeanPool.ZhangYeungInequality.Test.Theorem5
LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Lift
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.PreLift
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Strat
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.Lift
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.PreLift
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.Strat
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.TreeLift
LeanPool.AndersonConjecture.Jensen.Adjoin.Adjoin
LeanPool.AndersonConjecture.Jensen.Adjoin.FromPrime
LeanPool.AndersonConjecture.Jensen.Adjoin.Transcendental
LeanPool.AndersonConjecture.Jensen.CloseUp.AvoidanceStep
LeanPool.AndersonConjecture.Jensen.CloseUp.Base
LeanPool.AndersonConjecture.Jensen.CloseUp.CloseUp
LeanPool.AndersonConjecture.Jensen.CloseUp.CoprimeSplit
LeanPool.AndersonConjecture.Jensen.CloseUp.Factor
LeanPool.AndersonConjecture.Jensen.CloseUp.FactorDivisibility
LeanPool.AndersonConjecture.Jensen.CloseUp.GcdComplexity
LeanPool.AndersonConjecture.Jensen.CloseUp.IntersectionHelpers
LeanPool.AndersonConjecture.Jensen.CloseUp.IntersectionStep
LeanPool.AndersonConjecture.Jensen.CloseUp.NoCommonFactor
LeanPool.AndersonConjecture.Jensen.CloseUp.TwoGen
LeanPool.AndersonConjecture.Jensen.Construction.ChainHelpers
LeanPool.AndersonConjecture.Jensen.Construction.Construction
LeanPool.AndersonConjecture.Jensen.Construction.HeitmannProp
LeanPool.AndersonConjecture.Jensen.Construction.Transfinite
LeanPool.AndersonConjecture.Jensen.KrullDomain.AdjoinLocSet
LeanPool.AndersonConjecture.Jensen.KrullDomain.HeightBound
LeanPool.AndersonConjecture.Jensen.KrullDomain.KrullDomain
LeanPool.AndersonConjecture.Jensen.KrullDomain.LocUFD
LeanPool.AndersonConjecture.Jensen.KrullDomain.Nagata
LeanPool.AndersonConjecture.Jensen.KrullDomain.Prime
LeanPool.AndersonConjecture.Jensen.KrullDomain.UFDConstruction
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.BoxPlusRealRoots
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Continuity
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Defs
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Density
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.HarmonicBound
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.InvPhiN
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Obreschkoff
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.ObreschkoffTransport
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.PhiN
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.RPoly
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.RealRoots
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Residue
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.RootContinuity
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.SignSquarefree
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.Transport
LeanPool.ArchonFirstProofResults.FirstProof4.Auxiliary.TransportDecomp
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.BarrierPotential
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.ColoringFramework
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.DynamicColoring
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.LaplacianBasics
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.LoewnerPullback
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.OneSidedBarrier
LeanPool.ArchonFirstProofResults.FirstProof6.Auxiliary.ResolventBound
LeanPool.BrauerGroupNew.Examples.ShortComplex.LeftHomologyMapData
LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra
LeanPool.BrauerGroupNew.Mathlib.Data.DFinsupp
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.LinearIndependent
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Span
LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory.Homological
LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence
LeanPool.BrauerGroupNew.Mathlib.RingTheory.MatrixAlgebra
LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubring
LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TensorProduct
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal
LeanPool.Circuitlib.Circuit.Belnap.Basic
LeanPool.Circuitlib.Circuit.Belnap.Gate
LeanPool.Circuitlib.Circuit.Belnap.Level
LeanPool.Circuitlib.Circuit.Category.Basic
LeanPool.Circuitlib.Circuit.Category.Combinational
LeanPool.Circuitlib.Circuit.Category.Sequential
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactOperatorOrthonormal
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint
LeanPool.CompactSpectral.Analysis.InnerProductSpace.RayleighCompact
LeanPool.EcTateLean.Algebra.CharP.Basic
LeanPool.EcTateLean.Algebra.EllipticCurve.AuxRingLemmas
LeanPool.EcTateLean.Algebra.EllipticCurve.KodairaTypes
LeanPool.EcTateLean.Algebra.EllipticCurve.Kronecker
LeanPool.EcTateLean.Algebra.EllipticCurve.Model
LeanPool.EcTateLean.Algebra.Ring.Basic
LeanPool.ErdosTuzaValtr.Lib.Core.Rel3
LeanPool.ErdosTuzaValtr.Lib.List.Chain3
LeanPool.ErdosTuzaValtr.Lib.List.Default
LeanPool.ErdosTuzaValtr.Lib.List.Defs
LeanPool.ErdosTuzaValtr.Lib.List.Lemmas
LeanPool.ErdosTuzaValtr.Main.Lemmas.Default
LeanPool.ErdosTuzaValtr.Main.Lemmas.InterweavedLacedNgon
LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N2
LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3JoinN3N2
LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N3N2
LeanPool.FormalLearningTheory.Complexity.Generalization.Core
LeanPool.FormalLearningTheory.Complexity.Generalization.Tail
LeanPool.Incompleteness.Arithmetization.Basic.IOpen
LeanPool.Incompleteness.Arithmetization.Basic.Ind
LeanPool.Incompleteness.Arithmetization.Basic.PeanoMinus
LeanPool.Incompleteness.Arithmetization.Definability.Absoluteness
LeanPool.Incompleteness.Arithmetization.Definability.Boldface
LeanPool.Incompleteness.Arithmetization.Definability.BoundedBoldface
LeanPool.Incompleteness.Arithmetization.Definability.Hierarchy
LeanPool.Incompleteness.Arithmetization.Definability.Init
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Bit
LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath
LeanPool.Incompleteness.Arithmetization.Vorspiel.ExistsUnique
LeanPool.Incompleteness.Arithmetization.Vorspiel.Graph
LeanPool.Incompleteness.Arithmetization.Vorspiel.Lemmata
LeanPool.Incompleteness.Arithmetization.Vorspiel.Vorspiel
LeanPool.Incompleteness.Foundation.FirstOrder.Basic
LeanPool.Incompleteness.Foundation.FirstOrder.Ultraproduct
LeanPool.Incompleteness.Foundation.IntProp.Formula
LeanPool.Incompleteness.Foundation.IntProp.Substitution
LeanPool.Incompleteness.Foundation.Logic.Axioms
LeanPool.Incompleteness.Foundation.Logic.Calculus
LeanPool.Incompleteness.Foundation.Logic.Disjunctive
LeanPool.Incompleteness.Foundation.Logic.Entailment
LeanPool.Incompleteness.Foundation.Logic.LogicSymbol
LeanPool.Incompleteness.Foundation.Logic.Semantics
LeanPool.Incompleteness.Foundation.Modal.Axioms
LeanPool.Incompleteness.Foundation.Modal.Complement
LeanPool.Incompleteness.Foundation.Modal.ComplementClosedConsistentFinset
LeanPool.Incompleteness.Foundation.Modal.Formula
LeanPool.Incompleteness.Foundation.Modal.Geachean
LeanPool.Incompleteness.Foundation.Modal.IntProp
LeanPool.Incompleteness.Foundation.Modal.LogicSymbol
LeanPool.Incompleteness.Foundation.Modal.MaximalConsistentSet
LeanPool.Incompleteness.Foundation.Modal.Subformulas
LeanPool.Incompleteness.Foundation.Modal.Substitution
LeanPool.Incompleteness.Foundation.Vorspiel.Arith
LeanPool.Incompleteness.Foundation.Vorspiel.BinaryRelations
LeanPool.Incompleteness.Foundation.Vorspiel.Chain
LeanPool.Incompleteness.Foundation.Vorspiel.Collection
LeanPool.Incompleteness.Foundation.Vorspiel.ExistsUnique
LeanPool.Incompleteness.Foundation.Vorspiel.NotationClass
LeanPool.Incompleteness.Foundation.Vorspiel.Order
LeanPool.Incompleteness.Foundation.Vorspiel.RelItr
LeanPool.Incompleteness.Foundation.Vorspiel.Vorspiel
LeanPool.LeanComplexAnalysis.Harmonic.Positive.HarnackIneq
LeanPool.LeanComplexAnalysis.Harmonic.Positive.HerglotzRieszRepresentations
LeanPool.LeanComplexAnalysis.Harmonic.Positive.HerglotzRieszUnique
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy.Basic
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy.DixonProof
LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauchy.Meromorphic
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.CircleParam
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.Integrality
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.Invariance
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.MathlibBridge
LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.ParametricDiff
LeanPool.LeanModularForms.GeneralizedResidueTheory.OnCurvePV.Basic
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.AnnulusBounds
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.GammaAnalysis
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.RemainderAnalysis
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.SingularAnnulus
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.StepBounds
LeanPool.LeanModularForms.GeneralizedResidueTheory.PVInfrastructure.UniformStepBound
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.Flatness
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.GeneralizedTheorem
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.GeneralizedTheoremBase
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MathlibBridge
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MeasureHelpers
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MeromorphicLaurent
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MeromorphicPrincipalPart
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MultipointPV
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.SectorCurve
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.SectorCurveLemma
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.CrossingAnalysis
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.Decomposition
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.Defs
LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.Proposition22
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Associativity
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Basic
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Commutativity
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Degree
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Module
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Multiplication
LeanPool.LeanModularForms.HeckeRIngs.AbstractHeckeRing.Ring
LeanPool.LeanModularForms.HeckeRIngs.GL2.Basic
LeanPool.LeanModularForms.HeckeRIngs.GL2.CongruenceIndex
LeanPool.LeanModularForms.HeckeRIngs.GL2.Degree
LeanPool.LeanModularForms.HeckeRIngs.GL2.HeckeAction
LeanPool.LeanModularForms.HeckeRIngs.GL2.HeckeModularForm
LeanPool.LeanModularForms.HeckeRIngs.GL2.MultiplicationTable
LeanPool.LeanModularForms.HeckeRIngs.GLn.Basic
LeanPool.LeanModularForms.HeckeRIngs.GLn.CoprimeMul
LeanPool.LeanModularForms.HeckeRIngs.GLn.CosetDecomposition
LeanPool.LeanModularForms.HeckeRIngs.GLn.Degree
LeanPool.LeanModularForms.HeckeRIngs.GLn.DiagonalCosets
LeanPool.LeanModularForms.HeckeRIngs.GLn.PolynomialRing
LeanPool.LeanModularForms.HeckeRIngs.GLn.PrimeDecomposition
LeanPool.LeanModularForms.HeckeRIngs.GLn.SLnTransvection
LeanPool.LeanModularForms.HeckeRIngs.GLn.TransposeAntiInvolution
LeanPool.LeanModularForms.Modularforms.Generators.Defs
LeanPool.LeanModularForms.Modularforms.Generators.Injectivity
LeanPool.LeanModularForms.Modularforms.Generators.Surjectivity
LeanPool.LeanModularForms.ValenceFormula.Boundary.Basic
LeanPool.LeanModularForms.ValenceFormula.Boundary.Bounds
LeanPool.LeanModularForms.ValenceFormula.Boundary.Smooth
LeanPool.LeanModularForms.ValenceFormula.OnCurvePV.Basic
LeanPool.LeanModularForms.ValenceFormula.OnCurvePV.EndpointCorner
LeanPool.LeanModularForms.ValenceFormula.OnCurvePV.Main
LeanPool.LeanModularForms.ValenceFormula.PVChain.ArcContribution
LeanPool.LeanModularForms.ValenceFormula.PVChain.Assembly
LeanPool.LeanModularForms.ValenceFormula.PVChain.Helpers
LeanPool.LeanModularForms.ValenceFormula.PVChain.OnCurveCapture
LeanPool.LeanModularForms.ValenceFormula.PVChain.ResidueSideInfra
LeanPool.LeanModularForms.ValenceFormula.PVChain.Seg5CuspIntegral
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.AngleAnalysis
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.BoundaryHomotopyDerivBounds
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.BoundaryHomotopyDiff
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.BoundaryHomotopySmooth
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.Geometry
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.HomotopyDef
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.MainTheorem
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.MainTheoremBound
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.MainTheoremDerivCont
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.PolygonProps
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.PolygonSlope
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.RadialHomotopy
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.WindingBase
LeanPool.LeanModularForms.ValenceFormula.RectHomotopy.WindingProof
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.Common
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.I
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.Rho
LeanPool.LeanModularForms.ValenceFormula.WindingWeights.RhoPlusOne
LeanPool.LeanQuantumAlg.Core.Components.Control
LeanPool.LeanQuantumAlg.Core.Components.Gates
LeanPool.LeanQuantumAlg.Core.Components.Kets
LeanPool.LeanQuantumAlg.Core.Components.Oracle
LeanPool.LeanQuantumAlg.Primitives.QKernel.Advantage
LeanPool.LeanQuantumAlg.Primitives.QKernel.Concentration
LeanPool.LeanQuantumAlg.Primitives.QKernel.DiscreteLogConcept
LeanPool.LeanQuantumAlg.Primitives.QKernel.Expressivity
LeanPool.LeanQuantumAlg.Primitives.QKernel.Fidelity
LeanPool.LeanQuantumAlg.Primitives.QKernel.Fourier
LeanPool.LeanQuantumAlg.Primitives.QNN.DynamicalLieAlgebra
LeanPool.LeanQuantumAlg.Primitives.QNN.FullDLABasis
LeanPool.LeanQuantumAlg.Primitives.QNN.LieAlgebraicBP
LeanPool.LeanQuantumAlg.Primitives.QNN.Overparametrization
LeanPool.LeanQuantumAlg.Primitives.QNN.PauliPropagation
LeanPool.LeanQuantumAlg.Primitives.QNN.Trainability
LeanPool.LeanQuantumAlg.Primitives.QNN.VarianceFormula
LeanPool.LeanQuantumAlg.Primitives.QSP.Chebyshev
LeanPool.LeanQuantumAlg.Primitives.QSP.Fourier
LeanPool.Lentil.ProofMode.Tactics.Apply
LeanPool.Lentil.ProofMode.Tactics.Assumption
LeanPool.Lentil.ProofMode.Tactics.CheckGoalForm
LeanPool.Lentil.ProofMode.Tactics.Clear
LeanPool.Lentil.ProofMode.Tactics.CoalesceToPTL
LeanPool.Lentil.ProofMode.Tactics.Contradiction
LeanPool.Lentil.ProofMode.Tactics.Exists
LeanPool.Lentil.ProofMode.Tactics.Exit
LeanPool.Lentil.ProofMode.Tactics.Have
LeanPool.Lentil.ProofMode.Tactics.Intro
LeanPool.Lentil.ProofMode.Tactics.LeftRight
LeanPool.Lentil.ProofMode.Tactics.ModalityMisc
LeanPool.Lentil.ProofMode.Tactics.Monotone
LeanPool.Lentil.ProofMode.Tactics.Normalize
LeanPool.Lentil.ProofMode.Tactics.PurePred
LeanPool.Lentil.ProofMode.Tactics.RCases
LeanPool.Lentil.ProofMode.Tactics.Rename
LeanPool.Lentil.ProofMode.Tactics.Revert
LeanPool.Lentil.ProofMode.Tactics.Rewrite
LeanPool.Lentil.ProofMode.Tactics.Simp
LeanPool.Lentil.ProofMode.Tactics.Specialize
LeanPool.Lentil.ProofMode.Tactics.SplitAnds
LeanPool.Lentil.ProofMode.Tactics.Start
LeanPool.MisereGames.Form.Misere.Adjoint
LeanPool.MisereGames.Form.Misere.Outcome
LeanPool.MisereGames.Misere.Hereditary.MaintenanceProviso
LeanPool.MisereGames.Misere.OutcomeStable.PropertyX
LeanPool.Monlib4.LinearAlgebra.Coalgebra.FiniteDimensional
LeanPool.Monlib4.LinearAlgebra.Coalgebra.Lemmas
LeanPool.Monlib4.LinearAlgebra.Coalgebra.MulOpposite
LeanPool.Monlib4.LinearAlgebra.Ips.Basic
LeanPool.Monlib4.LinearAlgebra.Ips.Frob
LeanPool.Monlib4.LinearAlgebra.Ips.Functional
LeanPool.Monlib4.LinearAlgebra.Ips.Ips
LeanPool.Monlib4.LinearAlgebra.Ips.MatIps
LeanPool.Monlib4.LinearAlgebra.Ips.MinimalProj
LeanPool.Monlib4.LinearAlgebra.Ips.MulOp
LeanPool.Monlib4.LinearAlgebra.Ips.Nontracial
LeanPool.Monlib4.LinearAlgebra.Ips.OpUnop
LeanPool.Monlib4.LinearAlgebra.Ips.Pos
LeanPool.Monlib4.LinearAlgebra.Ips.RankOne
LeanPool.Monlib4.LinearAlgebra.Ips.Strict
LeanPool.Monlib4.LinearAlgebra.Ips.Symm
LeanPool.Monlib4.LinearAlgebra.Ips.TensorHilbert
LeanPool.Monlib4.LinearAlgebra.Ips.Vn
LeanPool.Monlib4.LinearAlgebra.Matrix.Basic
LeanPool.Monlib4.LinearAlgebra.Matrix.Cast
LeanPool.Monlib4.LinearAlgebra.Matrix.Conj
LeanPool.Monlib4.LinearAlgebra.Matrix.IncludeBlock
LeanPool.Monlib4.LinearAlgebra.Matrix.IsAlmostHermitian
LeanPool.Monlib4.LinearAlgebra.Matrix.PiMat
LeanPool.Monlib4.LinearAlgebra.Matrix.PosDefRpow
LeanPool.Monlib4.LinearAlgebra.Matrix.PosEqLinearMapIsPositive
LeanPool.Monlib4.LinearAlgebra.Matrix.Reshape
LeanPool.Monlib4.LinearAlgebra.Matrix.Spectra
LeanPool.Monlib4.LinearAlgebra.Matrix.StarOrderedRing
LeanPool.Monlib4.LinearAlgebra.QuantumSet.Basic
LeanPool.Monlib4.LinearAlgebra.QuantumSet.DeltaForm
LeanPool.Monlib4.LinearAlgebra.QuantumSet.Instances
LeanPool.Monlib4.LinearAlgebra.QuantumSet.PhiMap
LeanPool.Monlib4.LinearAlgebra.QuantumSet.Pi
LeanPool.Monlib4.LinearAlgebra.QuantumSet.QIso
LeanPool.Monlib4.LinearAlgebra.QuantumSet.SchurMul
LeanPool.Monlib4.LinearAlgebra.QuantumSet.SchurMulTensor
LeanPool.Monlib4.LinearAlgebra.QuantumSet.Subset
LeanPool.Monlib4.LinearAlgebra.QuantumSet.Symm
LeanPool.Monlib4.LinearAlgebra.QuantumSet.TensorProduct
LeanPool.Monlib4.LinearAlgebra.TensorProduct.BasicLemmas
LeanPool.Monlib4.LinearAlgebra.TensorProduct.FiniteDimensional
LeanPool.Monlib4.LinearAlgebra.TensorProduct.Lemmas
LeanPool.Monlib4.LinearAlgebra.TensorProduct.OrthonormalBasis
LeanPool.Monlib4.LinearAlgebra.TensorProduct.Submodule
LeanPool.OSforGFF.GaussianField.Nuclear.DyninMityagin
LeanPool.OSforGFF.GaussianField.Nuclear.NuclearSpace
LeanPool.OSforGFF.GaussianField.Nuclear.NuclearTensorProduct
LeanPool.OSforGFF.GaussianField.SchwartzNuclear.Basis1D
LeanPool.OSforGFF.GaussianField.SchwartzNuclear.HermiteFunctions
LeanPool.OSforGFF.GaussianField.SchwartzNuclear.HermiteNuclear
LeanPool.OSforGFF.GaussianField.SchwartzNuclear.HermiteTensorProduct
LeanPool.OSforGFF.GaussianField.SchwartzNuclear.ParametricCalculus
LeanPool.OSforGFF.GaussianField.SchwartzNuclear.SchwartzHermiteExpansion
LeanPool.OSforGFF.GaussianField.SchwartzNuclear.SchwartzSlicing
LeanPool.PLAcceleratedNesterovLean.Convergence.Bootstrap.Main
LeanPool.PLAcceleratedNesterovLean.Convergence.Bootstrap.Step1
LeanPool.PLAcceleratedNesterovLean.Convergence.Bootstrap.Step2
LeanPool.PLAcceleratedNesterovLean.Convergence.Coercivity.Core
LeanPool.PLAcceleratedNesterovLean.Convergence.Coercivity.Main
LeanPool.PLAcceleratedNesterovLean.Convergence.Coercivity.Step1
LeanPool.PLAcceleratedNesterovLean.Convergence.Coercivity.Step2
LeanPool.PLAcceleratedNesterovLean.Convergence.CurvAbsorb.Algebraic
LeanPool.PLAcceleratedNesterovLean.Convergence.CurvAbsorb.Assembly
LeanPool.PLAcceleratedNesterovLean.Convergence.LocalGeometry.HessianBound
LeanPool.PLAcceleratedNesterovLean.Convergence.LocalGeometry.Main
LeanPool.PLAcceleratedNesterovLean.Convergence.LocalGeometry.SegmentEstimate
LeanPool.PLAcceleratedNesterovLean.Convergence.LocalGeometry.Step1
LeanPool.PLAcceleratedNesterovLean.Convergence.LocalGeometry.Step2
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.AuxVar
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.FlatCaseArithmetic
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.FlatCaseHelper
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.GenMain
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.Main
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.Step1
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.Step2
LeanPool.PLAcceleratedNesterovLean.Convergence.LyapunovContraction.Step3
LeanPool.PLAcceleratedNesterovLean.Convergence.MotionError.Main
LeanPool.PLAcceleratedNesterovLean.Convergence.StateContraction.AuxVarRecursion
LeanPool.PLAcceleratedNesterovLean.MorseBott.HessianPL.Basics
LeanPool.PLAcceleratedNesterovLean.MorseBott.HessianPL.Main
LeanPool.PLAcceleratedNesterovLean.MorseBott.TubularProjection.Defs
LeanPool.PLAcceleratedNesterovLean.MorseBott.TubularProjection.Derivative
LeanPool.PLAcceleratedNesterovLean.MorseBott.TubularProjection.IFT
LeanPool.PhaseRetrieval.Constant.Internal.AnnulusLocalEstimate
LeanPool.PhaseRetrieval.Constant.Internal.BlockDecomposition
LeanPool.PhaseRetrieval.Constant.Internal.Definitions
LeanPool.PhaseRetrieval.Constant.Internal.HighFreqBandEstimate
LeanPool.PhaseRetrieval.Constant.Internal.LaplaceFactorial
LeanPool.PhaseRetrieval.Constant.Internal.LeakageEstimate
LeanPool.PhaseRetrieval.Constant.Internal.LipschitzRho
LeanPool.PhaseRetrieval.Constant.Internal.Local
LeanPool.PhaseRetrieval.Constant.Internal.LocalCircleEstimate
LeanPool.PhaseRetrieval.Constant.Internal.LocalCore
LeanPool.PhaseRetrieval.Constant.Internal.LocalHelpers
LeanPool.PhaseRetrieval.Constant.Internal.MainTheorem
LeanPool.PhaseRetrieval.Constant.Internal.RotationalAveraging
LeanPool.PhaseRetrieval.Constant.Internal.SafeSquare
LeanPool.PhaseRetrieval.DimdPoly.Internal.Auxiliary
LeanPool.PhaseRetrieval.DimdPoly.Internal.CoefficientLimitRigidity
LeanPool.PhaseRetrieval.DimdPoly.Internal.Definitions
LeanPool.PhaseRetrieval.DimdPoly.Internal.ExactModulusRecovery
LeanPool.PhaseRetrieval.DimdPoly.Internal.FiniteBaseAnnulusEstimate
LeanPool.PhaseRetrieval.DimdPoly.Internal.FiniteBaseCircleEstimate
LeanPool.PhaseRetrieval.DimdPoly.Internal.ImportedAnalyticInputs
LeanPool.PhaseRetrieval.DimdPoly.Internal.OrthogonalCoercivity
LeanPool.PhaseRetrieval.DimdPoly.Internal.PhaseStability
LeanPool.PhaseRetrieval.DimdPoly.Internal.ProductAnnulusLocalization
LeanPool.PhaseRetrieval.DimdPoly.Internal.TensorBasis
LeanPool.Polylean.Complexes.Constructions.UniversalCover
LeanPool.Polylean.Complexes.Structures.Category
LeanPool.Polylean.Complexes.Structures.FreeGroupoid
LeanPool.Polylean.Complexes.Structures.Groupoid
LeanPool.Polylean.Complexes.Structures.Invertegory
LeanPool.Polylean.Complexes.Structures.Quiver
LeanPool.Polylean.Complexes.Structures.TwoComplex
LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets
LeanPool.Polylean.UnitConjecture.Tactics.ReduceGoal
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain.Const
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain.Option
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain.Sigma
LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain.Sum
LeanPool.RlTheoryInLean.Analysis.Normed.Group
LeanPool.RlTheoryInLean.Data.Matrix.Mul
LeanPool.RlTheoryInLean.Data.Matrix.PosDef
LeanPool.RlTheoryInLean.Data.Matrix.Stochastic
LeanPool.RlTheoryInLean.MeasureTheory.Function.ConditionalExpectation
LeanPool.RlTheoryInLean.MeasureTheory.Function.L1Space
LeanPool.RlTheoryInLean.MeasureTheory.MeasurableSpace.Constructions
LeanPool.RlTheoryInLean.MeasureTheory.Measure.GiryMonad
LeanPool.RlTheoryInLean.MeasureTheory.Measure.Prod
LeanPool.RlTheoryInLean.Order.Filter.Basic
LeanPool.RlTheoryInLean.Probability.Kernel.Basic
LeanPool.RlTheoryInLean.Probability.Kernel.Composition
LeanPool.RlTheoryInLean.Probability.MarkovChain.Defs
LeanPool.RlTheoryInLean.Probability.MarkovChain.Finite
LeanPool.RlTheoryInLean.Probability.MarkovChain.Trajectory
LeanPool.SingularModuli.QuadraticOrder.Prime.Inert
LeanPool.SingularModuli.QuadraticOrder.Prime.PolyMod
LeanPool.SingularModuli.QuadraticOrder.Prime.QuotientIso
LeanPool.SingularModuli.QuadraticOrder.Prime.Ramified
LeanPool.SingularModuli.QuadraticOrder.Prime.Split
LeanPool.TwoColoringOneRound.UpperBound.Recursive3Param.Basic
LeanPool.TwoColoringOneRound.UpperBound.Recursive3Param.Bound
LeanPool.TwoColoringOneRound.UpperBound.Recursive3Param.ComputeP
LeanPool.TwoColoringOneRound.UpperBound.Recursive3Param.Final
LeanPool.TwoColoringOneRound.UpperBound.Recursive3Param.Regions
LeanPool.TwoColoringOneRound.UpperBound.Recursive3Param.Value
LeanPool.VirasoroProject.ToMathlib.Algebra.Lie
LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Basis
LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Finsupp
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra
LeanPool.VirasoroProject.ToMathlib.Topology.Order
LeanPool.WhiteheadTheorem.CWComplex.IProd.Def
LeanPool.WhiteheadTheorem.CWComplex.IProd.Iso
LeanPool.ZhangYeungInequality.PFR.ForMathlib.ConditionalIndependence
LeanPool.ZhangYeungInequality.PFR.ForMathlib.Pair
LeanPool.ZhangYeungInequality.PFR.ForMathlib.Uniform
LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Equiv
LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra
LeanPool.BrauerGroupNew.Mathlib.Data.DFinsupp.Submonoid
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.LinearIndependent.Defs
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.Charpoly
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Span.Basic
LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory.Homological.GroupCohomology
LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence.Basic
LeanPool.BrauerGroupNew.Mathlib.RingTheory.Congruence.Defs
LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubring.Defs
LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring.Basic
LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring.Defs
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TensorProduct.Basic
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Basic
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Kernel
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Lattice
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Operations
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.Approximation
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.Basic
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.CutoffProjector
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.OpNormEigenvalue
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.SpectralFiniteness
LeanPool.CompactSpectral.Analysis.InnerProductSpace.CompactSelfAdjoint.SpectralTheorem
LeanPool.EcTateLean.Init.Data.Int.Lemmas
LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.Basic
LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.Coding
LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.Fixpoint
LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.PRF
LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.Seq
LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.Vec
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.CodedTheory
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Coding
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Language
LeanPool.Incompleteness.Arithmetization.ISigmaZero.Exponential.Exp
LeanPool.Incompleteness.Arithmetization.ISigmaZero.Exponential.Log
LeanPool.Incompleteness.Arithmetization.ISigmaZero.Exponential.PPow2
LeanPool.Incompleteness.Arithmetization.ISigmaZero.Exponential.Pow2
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.Basic
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.CobhamR0
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.Hierarchy
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.Model
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.PeanoMinus
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.Representation
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.StrictHierarchy
LeanPool.Incompleteness.Foundation.FirstOrder.Arith.Theory
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.BinderNotation
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Calculus
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Calculus2
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Coding
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Eq
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Model
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Operator
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Soundness
LeanPool.Incompleteness.Foundation.FirstOrder.Completeness.Coding
LeanPool.Incompleteness.Foundation.FirstOrder.Completeness.Completeness
LeanPool.Incompleteness.Foundation.FirstOrder.Completeness.Corollaries
LeanPool.Incompleteness.Foundation.FirstOrder.Completeness.SearchTree
LeanPool.Incompleteness.Foundation.FirstOrder.Completeness.SubLanguage
LeanPool.Incompleteness.Foundation.FirstOrder.Order.Le
LeanPool.Incompleteness.Foundation.IntProp.Hilbert.Basic
LeanPool.Incompleteness.Foundation.IntProp.Hilbert.Int
LeanPool.Incompleteness.Foundation.IntProp.Hilbert.WellKnown
LeanPool.Incompleteness.Foundation.IntProp.Kripke.Basic
LeanPool.Incompleteness.Foundation.Logic.HilbertStyle.Basic
LeanPool.Incompleteness.Foundation.Logic.HilbertStyle.Context
LeanPool.Incompleteness.Foundation.Logic.HilbertStyle.Lukasiewicz
LeanPool.Incompleteness.Foundation.Logic.HilbertStyle.Supplemental
LeanPool.Incompleteness.Foundation.Logic.Predicate.Language
LeanPool.Incompleteness.Foundation.Logic.Predicate.Quantifier
LeanPool.Incompleteness.Foundation.Logic.Predicate.Rew
LeanPool.Incompleteness.Foundation.Logic.Predicate.Term
LeanPool.Incompleteness.Foundation.Modal.Entailment.Basic
LeanPool.Incompleteness.Foundation.Modal.Entailment.GL
LeanPool.Incompleteness.Foundation.Modal.Entailment.Grz
LeanPool.Incompleteness.Foundation.Modal.Entailment.K
LeanPool.Incompleteness.Foundation.Modal.Entailment.K4
LeanPool.Incompleteness.Foundation.Modal.Entailment.K5
LeanPool.Incompleteness.Foundation.Modal.Entailment.KD
LeanPool.Incompleteness.Foundation.Modal.Entailment.KP
LeanPool.Incompleteness.Foundation.Modal.Entailment.KT
LeanPool.Incompleteness.Foundation.Modal.Entailment.KTc
LeanPool.Incompleteness.Foundation.Modal.Entailment.S5
LeanPool.Incompleteness.Foundation.Modal.Entailment.Triv
LeanPool.Incompleteness.Foundation.Modal.Hilbert.Basic
LeanPool.Incompleteness.Foundation.Modal.Hilbert.Geach
LeanPool.Incompleteness.Foundation.Modal.Hilbert.K
LeanPool.Incompleteness.Foundation.Modal.Hilbert.S5Grz
LeanPool.Incompleteness.Foundation.Modal.Hilbert.WellKnown
LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomDot3
LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomGrz
LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomL
LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomVer
LeanPool.Incompleteness.Foundation.Modal.Kripke.Basic
LeanPool.Incompleteness.Foundation.Modal.Kripke.Closure
LeanPool.Incompleteness.Foundation.Modal.Kripke.Completeness
LeanPool.Incompleteness.Foundation.Modal.Kripke.Filteration
LeanPool.Incompleteness.Foundation.Modal.Kripke.FiniteFrame
LeanPool.Incompleteness.Foundation.Modal.Kripke.KHIncompleteness
LeanPool.Incompleteness.Foundation.Modal.Kripke.Preservation
LeanPool.Incompleteness.Foundation.Modal.Kripke.SimpleExtension
LeanPool.Incompleteness.Foundation.Modal.Kripke.Tree
LeanPool.Incompleteness.Foundation.Modal.Logic.Basic
LeanPool.Incompleteness.Foundation.Modal.Logic.WellKnown
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.BoundaryVanishing
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.CPVExistence
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.CutoffInfrastructure
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.HigherOrderAssembly
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.PerTermVanishing
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.MultipointPV.DominatedConvergence
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.Framework
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.LeftEdge
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.RightEdge
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.UnitArc
LeanPool.LeanModularForms.ValenceFormula.Boundary.Winding.UnitArcHelpers
LeanPool.LeanModularForms.ValenceFormula.PVChain.Assembly.ResidueSide
LeanPool.PhaseRetrieval.Constant.Internal.MissingMathlib.Poincare
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite.Definitions
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite.ImportedAnalyticInputs
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite.MissingMathlib
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite1Dimd.BlockLocalization
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite1Dimd.Definitions
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite1Dimd.DegreeBookkeeping
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite1Dimd.ImportedAnalyticInputs
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite1Dimd.ProductAnnulusCircle
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermite1Dimd.ProductBasisAndAnnuli
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermitek.BasisLocalization
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermitek.ImportedAnalyticInputs
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermitek.ModulusRigidity
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermitek.TrueLevelBasis
LeanPool.PhaseRetrieval.DimdPoly.Internal.OrthogonalReduction.OrthogonalReduction
LeanPool.RlTheoryInLean.Analysis.Normed.Group.Basic
LeanPool.RlTheoryInLean.MeasureTheory.Function.ConditionalExpectation.Basic
LeanPool.RlTheoryInLean.MeasureTheory.Function.L1Space.Integrable
LeanPool.RlTheoryInLean.Probability.Kernel.Composition.MapComap
LeanPool.RlTheoryInLean.Probability.MarkovChain.Finite.Defs
LeanPool.VirasoroProject.ToMathlib.Algebra.Lie.Abelian
LeanPool.VirasoroProject.ToMathlib.Algebra.Lie.Basic
LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Basis.Defs
LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Basis.FinsumRepr
LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Finsupp.Supported
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.BigOperators
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.ConstMulAction
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.InfiniteSum
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.Module
LeanPool.ZhangYeungInequality.PFR.ForMathlib.Entropy.Basic
LeanPool.ZhangYeungInequality.PFR.ForMathlib.Entropy.Measure
LeanPool.ZhangYeungInequality.PFR.ForMathlib.FiniteRange.ConditionalProbability
LeanPool.ZhangYeungInequality.PFR.ForMathlib.FiniteRange.Defs
LeanPool.ZhangYeungInequality.PFR.Mathlib.Probability.ConditionalProbability
LeanPool.ZhangYeungInequality.PFR.Mathlib.Probability.IdentDistrib
LeanPool.ZhangYeungInequality.PFR.Mathlib.Probability.UniformOn
LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra.Basic
LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra.Directed
LeanPool.BrauerGroupNew.Mathlib.Algebra.Algebra.Subalgebra.Lattice
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
LeanPool.BrauerGroupNew.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
LeanPool.BrauerGroupNew.Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Formula.Basic
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Formula.Functions
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Formula.Iteration
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Formula.Typed
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Proof.Derivation
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Proof.Thy
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Proof.Typed
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Term.Basic
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Term.Functions
LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Term.Typed
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Semantics.Elementary
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Semantics.Semantics
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Syntax.Formula
LeanPool.Incompleteness.Foundation.FirstOrder.Basic.Syntax.Rew
LeanPool.Incompleteness.Foundation.IntProp.Kripke.Hilbert.Soundness
LeanPool.Incompleteness.Foundation.Modal.Hilbert.Maximal.Basic
LeanPool.Incompleteness.Foundation.Modal.Hilbert.Maximal.Unprovability
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Geach
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.K
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.K4
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.K45
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.K5
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KB
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KB4
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KB5
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KD
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KD4
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KD45
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KD5
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KDB
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KT
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KT4B
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.KTB
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.S4
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.S4Dot2
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.S4Dot3
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.S5
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Soundness
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Triv
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Ver
LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransfer.PerTermVanishing.CPVHelpers
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.BigOperators.FinProd
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.InfiniteSum.Basic
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.Module.LinearMap
LeanPool.ZhangYeungInequality.PFR.ForMathlib.Entropy.Kernel.Basic
LeanPool.ZhangYeungInequality.PFR.ForMathlib.Entropy.Kernel.MutualInfo
LeanPool.ZhangYeungInequality.PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
LeanPool.ZhangYeungInequality.PFR.Mathlib.Data.Set.Basic
LeanPool.ZhangYeungInequality.PFR.Mathlib.Data.Set.Card
LeanPool.ZhangYeungInequality.PFR.Mathlib.Data.Set.Insert
LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Constructions.Pi
LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Measure.Dirac
LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Measure.Prod
LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Measure.Real
LeanPool.ZhangYeungInequality.PFR.Mathlib.Probability.Independence.Basic
LeanPool.ZhangYeungInequality.PFR.Mathlib.Probability.Kernel.Disintegration
LeanPool.Incompleteness.Foundation.IntProp.Kripke.Hilbert.Cl.Basic
LeanPool.Incompleteness.Foundation.IntProp.Kripke.Hilbert.Cl.Classical
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Completeness
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.MDP
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Soundness
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Tree
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Unnecessitation
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Grz.Completeness
LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.Grz.Soundness
LeanPool.VirasoroProject.ToMathlib.Topology.Algebra.Module.LinearMap.Defs
LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic
LeanPool.ZhangYeungInequality.PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable
LeanPool.ZhangYeungInequality.PFR.Mathlib.Probability.Independence.Kernel.IndepFun
LeanPool.ZhangYeungInequality.PFR.Mathlib.Probability.Kernel.Composition.Comp
Imported by