1000+ Theorems project

Theorem	Software	Paper
continuum hypothesis	Lean	A Formal Proof of the Independence of the Continuum Hypothesis

About

 The spiritual successor of Freek’s list of 100 theorems. Now with more than 1000 theorems!
 The entries of this list are extracted from Wikipedia’s List of Theorems. We do not accept entries that are not part of that list.
 This project was initiated at the Special Trimester on “Prospects of Formalized Mathematics” at the Hausdorff Institute of Mathematics in Bonn, funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) under Germany ́s Excellence Strategy – EXC-2047/1 – 390685813.

source https://1000-plus.github.io/

Discussion

• https://www.wikidata.org/wiki/Wikidata:WikiProject_Mathematics/1000%2BTheorems

Persons involved

Katja Berči

Floris van Doorn

current examples from zbMATH Open (contributed by O Teschke)

https://zbmath.org/7699435

This review might have pointer to some of the proofs, but I could not find references to lean objects in mathlib? at a first glance.

Links from MathLib to the literature (contributed by Aaruni Kaushik)

The following list was generated by the command

`grep -i '\]\[[a-zA-Z0-9]*]$' --recursive ./Mathlib | grep
-v "\[[0-9]\]" | sed 's/\(^.*:\)/\1/'  | sort -u | wc -l`

and relates to the lean bib file.

Extended content

./Mathlib/Algebra/ContinuedFractions/Basic.lean:- [Wall, H.S., *Analytic Theory of Continued Fractions*][wall2018analytic] ./Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean:- [*Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph*][hardy2008introduction] ./Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean:- [*Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph*][hardy2008introduction] ./Mathlib/Algebra/EuclideanDomain/Defs.lean:* [M. Nagata, *On Euclid algorithm*][MR541021] ./Mathlib/Algebra/EuclideanDomain/Defs.lean:* [Th. Motzkin, *The Euclidean algorithm*][MR32592] ./Mathlib/Algebra/Homology/DerivedCategory/Basic.lean:* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] ./Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean:* [Brian Conrad, Grothendieck duality and base change][conrad2000] ./Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean:* [Brian Conrad, Grothendieck duality and base change][conrad2000] ./Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean:* [Brian Conrad, Grothendieck duality and base change][conrad2000] ./Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean:complexes. Here, we follow the original definitions in [Verdiers's thesis, I.3][verdier1996] ./Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean:* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] ./Mathlib/Algebra/Homology/LocalCohomology.lean: applications*][brodmannsharp13] ./Mathlib/Algebra/Homology/LocalCohomology.lean:* [M. Hochster, *Local cohomology*][hochsterunpublished] ./Mathlib/Algebra/Homology/LocalCohomology.lean:* [R. Hartshorne, *Local cohomology: A seminar given by A. Grothendieck*][hartshorne61] ./Mathlib/Algebra/Homology/LocalCohomology.lean: *Twenty-four hours of local cohomology*][iyengaretal13] ./Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean:[J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean:[J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean:[J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean:[J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean: * [J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean:* [J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean:[J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean: * [J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean: * [J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] ./Mathlib/AlgebraicGeometry/Noetherian.lean:* [Robin Hartshorne, *Algebraic Geometry*][Har77] ./Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean:* [Robin Hartshorne, *Algebraic Geometry*][Har77] ./Mathlib/AlgebraicGeometry/StructureSheaf.lean:* [Robin Hartshorne, *Algebraic Geometry*][Har77] ./Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean:* [Albrecht Dold, Homology of Symmetric Products and Other Functors of Complexes][dold1958] ./Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean:* [Albrecht Dold, *Homology of Symmetric Products and Other Functors of Complexes*][dold1958] ./Mathlib/Algebra/Jordan/Basic.lean:* [Hanche-Olsen and Størmer, Jordan Operator Algebras][hancheolsenstormer1984] ./Mathlib/Algebra/Jordan/Basic.lean:* [McCrimmon, A taste of Jordan algebras][mccrimmon2004] ./Mathlib/Algebra/Order/Group/Lattice.lean:* [Banasiak, Banach Lattices in Applications][banasiak] ./Mathlib/Algebra/Order/Group/Lattice.lean:* [Birkhoff, Lattice-ordered Groups][birkhoff1942] ./Mathlib/Algebra/Order/Group/Lattice.lean:* [Bourbaki, Algebra II][bourbaki1981] ./Mathlib/Algebra/Order/Group/Lattice.lean:* [Fuchs, Partially Ordered Algebraic Systems][fuchs1963] ./Mathlib/Algebra/Order/Group/Lattice.lean:* [Zaanen, Lectures on "Riesz Spaces"][zaanen1966] ./Mathlib/Algebra/Order/Group/PosPart.lean:* [Banasiak, Banach Lattices in Applications][banasiak] ./Mathlib/Algebra/Order/Group/PosPart.lean:* [Birkhoff, Lattice-ordered Groups][birkhoff1942] ./Mathlib/Algebra/Order/Group/PosPart.lean:* [Bourbaki, Algebra II][bourbaki1981] ./Mathlib/Algebra/Order/Group/PosPart.lean:* [Fuchs, Partially Ordered Algebraic Systems][fuchs1963] ./Mathlib/Algebra/Order/Group/PosPart.lean:* [Zaanen, Lectures on "Riesz Spaces"][zaanen1966] ./Mathlib/Algebra/Ring/CentroidHom.lean:* [Jacobson, Structure of Rings][Jacobson1956] ./Mathlib/Algebra/Ring/CentroidHom.lean:* [McCrimmon, A taste of Jordan algebras][mccrimmon2004] ./Mathlib/Algebra/Star/CHSH.lean:* [Bell, *On the Einstein Podolsky Rosen Paradox*][MR3790629] ./Mathlib/Algebra/Star/CHSH.lean: *Proposed experiment to test local hidden-variable theories*][zbMATH06785026] ./Mathlib/Algebra/Star/CHSH.lean:* [Tsirelson, *Quantum generalizations of Bell's inequality*][MR577178] ./Mathlib/Algebra/Symmetrized.lean:* [Hanche-Olsen and Størmer, Jordan Operator Algebras][hancheolsenstormer1984] ./Mathlib/Algebra/Vertex/HVertexOperator.lean:* [R. Borcherds, *Vertex Algebras, Kac-Moody Algebras, and the Monster*][borcherds1986vertex] ./Mathlib/Algebra/Vertex/VertexOperator.lean: fields*][matsuo1997] ./Mathlib/Algebra/Vertex/VertexOperator.lean: * [G. Mason, *Vertex rings and Pierce bundles*][mason2017] ./Mathlib/Analysis/Calculus/Rademacher.lean:* [Pertti Mattila, Geometry of sets and measures in Euclidean spaces, Theorem 7.3][Federer1996] ./Mathlib/Analysis/Convex/Cone/Basic.lean:* [Stephen P. Boyd and Lieven Vandenberghe, *Convex Optimization*][boydVandenberghe2004] ./Mathlib/Analysis/Convex/Cone/Proper.lean:- [B. Gartner and J. Matousek, Cone Programming][gartnerMatousek] ./Mathlib/Analysis/Convex/Exposed.lean:See chapter 8 of [Barry Simon, *Convexity*][simon2011] ./Mathlib/Analysis/Convex/Extreme.lean:See chapter 8 of [Barry Simon, *Convexity*][simon2011] ./Mathlib/Analysis/Convex/Gauge.lean:* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] ./Mathlib/Analysis/Convex/Intrinsic.lean:* Chapter 8 of [Barry Simon, *Convexity*][simon2011] ./Mathlib/Analysis/Convex/KreinMilman.lean:See chapter 8 of [Barry Simon, *Convexity*][simon2011] ./Mathlib/Analysis/Convex/TotallyBounded.lean:* [Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/InnerProductSpace/OfNorm.lean:- [Jordan, P. and von Neumann, J., *On inner products in linear, metric spaces*][Jordan1935] ./Mathlib/Analysis/InnerProductSpace/Positive.lean:* [Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean:* [Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/LocallyConvex/Barrelled.lean:* [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/LocallyConvex/Basic.lean:* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] ./Mathlib/Analysis/LocallyConvex/Bounded.lean:* [Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean:* [Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/LocallyConvex/Polar.lean:* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] ./Mathlib/Analysis/LocallyConvex/StrongTopology.lean:* [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/LocallyConvex/WeakDual.lean:* [Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Analysis/Normed/Group/Seminorm.lean:* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] ./Mathlib/Analysis/Normed/Module/Dual.lean:* [Conway, John B., A course in functional analysis][conway1990] ./Mathlib/Analysis/Normed/Operator/Compact.lean:* [N. Bourbaki, *Théories Spectrales*, Chapitre 3][bourbaki2023] ./Mathlib/Analysis/Normed/Order/Lattice.lean:* [Meyer-Nieberg, Banach lattices][MeyerNieberg1991] ./Mathlib/Analysis/NormedSpace/MStructure.lean:* [Behrends, M-structure and the Banach-Stone Theorem][behrends1979] ./Mathlib/Analysis/NormedSpace/MStructure.lean:* [Harmand, Werner, Werner, M-ideals in Banach spaces and Banach algebras][harmandwernerwerner1993] ./Mathlib/Analysis/Seminorm.lean:* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] ./Mathlib/CategoryTheory/Abelian/Basic.lean:* [P. Aluffi, *Algebra: Chapter 0*][aluffi2016] ./Mathlib/CategoryTheory/Abelian/Generator.lean:* [Peter J Freyd, *Abelian Categories* (Theorem 3.37)][freyd1964abelian] ./Mathlib/CategoryTheory/Adhesive.lean:- [Stephen Lack and Paweł Sobociński, Adhesive Categories][adhesive2004] ./Mathlib/CategoryTheory/Bicategory/Coherence.lean: proof of normalization for monoids][beylin1996] ./Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean:* [Riehl, *Category theory in context*, Proposition 6.5.2][riehl2017] ./Mathlib/CategoryTheory/Dialectica/Basic.lean:* [Valeria de Paiva, The Dialectica Categories.][dialectica1989] ./Mathlib/CategoryTheory/Elements.lean:* [Emily Riehl, *Category Theory in Context*, Section 2.4][riehl2017] ./Mathlib/CategoryTheory/Extensive.lean:- [Carboni et al, Introduction to extensive and distributive categories][CARBONI1993145] ./Mathlib/CategoryTheory/GuitartExact/Basic.lean:* [Bruno Kahn and Georges Maltsiniotis, *Structures de dérivabilité*][KahnMaltsiniotis2008] ./Mathlib/CategoryTheory/GuitartExact/Basic.lean:* [René Guitart, *Relations et carrés exacts*][Guitart1980] ./Mathlib/CategoryTheory/Limits/Presheaf.lean:* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92] ./Mathlib/CategoryTheory/Limits/VanKampen.lean:- [Stephen Lack and Paweł Sobociński, Adhesive Categories][adhesive2004] ./Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean:* [Bruno Kahn and Georges Maltsiniotis, *Structures de dérivabilité*][KahnMaltsiniotis2008] ./Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean:* [Bruno Kahn and Georges Maltsiniotis, *Structures de dérivabilité*][KahnMaltsiniotis2008] ./Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean:* [Bruno Kahn and Georges Maltsiniotis, *Structures de dérivabilité*][KahnMaltsiniotis2008] ./Mathlib/CategoryTheory/Localization/Resolution.lean:* [Bruno Kahn and Georges Maltsiniotis, *Structures de dérivabilité*][KahnMaltsiniotis2008] ./Mathlib/CategoryTheory/Localization/Triangulated.lean:* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] ./Mathlib/CategoryTheory/Monad/Algebra.lean:* [Riehl, *Category theory in context*, Section 5.2.4][riehl2017] ./Mathlib/CategoryTheory/Monad/Kleisli.lean:* [Riehl, *Category theory in context*, Definition 5.2.9][riehl2017] ./Mathlib/CategoryTheory/Monad/Limits.lean:-- Dual to theorem 5.6.5 from [Riehl][riehl2017] ./Mathlib/CategoryTheory/Monad/Limits.lean:-- Theorem 5.6.5 from [Riehl][riehl2017] ./Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean:* [Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, Victor Ostrik, *Tensor categories*][egno15] ./Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean: proof of normalization for monoids][beylin1996] ./Mathlib/CategoryTheory/Shift/CommShift.lean:* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] ./Mathlib/CategoryTheory/Sites/Closed.lean:* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92] ./Mathlib/CategoryTheory/Sites/CoverLifting.lean:* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92] ./Mathlib/CategoryTheory/Sites/Grothendieck.lean:* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92] ./Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean:* [J. Frenkel, *Cohomologie non abélienne et espaces fibrés*][frenkel1957] ./Mathlib/CategoryTheory/Sites/Pretopology.lean:* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92] ./Mathlib/CategoryTheory/Sites/Spaces.lean:* [S. MacLane, I. Moerdijk, *Sheaves in Geometry and Logic*][MM92] ./Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean:* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] ./Mathlib/CategoryTheory/Triangulated/Opposite.lean:* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] ./Mathlib/CategoryTheory/Triangulated/Subcategory.lean:* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] ./Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean:* [Giorgis Petridis, *The Plünnecke-Ruzsa inequality: an overview*][petridis2014] ./Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean:* [Aigner, *Combinatorial Theory, Chapter IV*][aigner1997] ./Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean:* [Jacobson, *Basic Algebra I, 8.6*][jacobson1974] ./Mathlib/Combinatorics/Optimization/ValuedCSP.lean: *An Algebraic Theory of Complexity for Discrete Optimisation*][cohen2012] ./Mathlib/Combinatorics/Schnirelmann.lean:* [Ruzsa, Imre, *Sumsets and structure*][ruzsa2009] ./Mathlib/Combinatorics/SetFamily/FourFunctions.lean:[*Applications of the FKG Inequality and Its Relatives*, Graham][Graham1983] ./Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean:* [D. J. Kleitman, *Families of non-disjoint subsets*][kleitman1966] ./Mathlib/Combinatorics/SetFamily/Intersecting.lean:* [D. J. Kleitman, *Families of non-disjoint subsets*][kleitman1966] ./Mathlib/Combinatorics/SetFamily/Kleitman.lean:* [D. J. Kleitman, *Families of non-disjoint subsets*][kleitman1966] ./Mathlib/Computability/Halting.lean:* [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019] ./Mathlib/Computability/PartrecCode.lean:* [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019] ./Mathlib/Computability/Partrec.lean:* [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019] ./Mathlib/Computability/Primrec.lean:* [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019] ./Mathlib/Computability/Reduce.lean:* [Robert Soare, *Recursively enumerable sets and degrees*][soare1987] ./Mathlib/Data/Finset/Sups.lean:[B. Bollobás, *Combinatorics*][bollobas1986] ./Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean:* [Cox, Little and O'Shea, *Ideals, varieties, and algorithms*][coxlittleoshea1997] ./Mathlib/Data/Finsupp/MonomialOrder.lean:* [Cox, Little and O'Shea, *Ideals, varieties, and algorithms*][coxlittleoshea1997] ./Mathlib/Data/List/Palindrome.lean:* [Pierre Castéran, *On palindromes*][casteran] ./Mathlib/Data/Matroid/Map.lean:* [E. Aigner-Horev, J. Carmesin, J. Fröhlic, Infinite Matroid Union][aignerhorev2012infinite] ./Mathlib/Data/Matroid/Map.lean:* [H. Perfect, Independence Spaces and Combinatorial Problems][perfect1969matroid] ./Mathlib/Data/Matroid/Map.lean:* [J. Oxley, Matroid Theory][oxley2011] ./Mathlib/Data/Set/Sups.lean:[B. Bollobás, *Combinatorics*][bollobas1986] ./Mathlib/FieldTheory/RatFunc/Defs.lean:* [Kleiman, *Misconceptions about $K_X$*][kleiman1979] ./Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean:* [Lee, J. M. (2012). _Introduction to Smooth Manifolds_. Springer New York.][lee2012] ./Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean:* [Lee, J. M. (2012). _Introduction to Smooth Manifolds_. Springer New York.][lee2012] ./Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean:* [Lee, J. M. (2012). _Introduction to Smooth Manifolds_. Springer New York.][lee2012] ./Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean:* [Lee, J. M. (2012). _Introduction to Smooth Manifolds_. Springer New York.][lee2012] ./Mathlib/GroupTheory/CoprodI.lean:[van der Waerden, *Free products of groups*][MR25465] ./Mathlib/GroupTheory/OreLocalization/Basic.lean:* [Zoran Škoda, *Noncommutative localization in noncommutative geometry*][skoda2006] ./Mathlib/LinearAlgebra/Basis/Cardinality.lean:-- From [Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973] ./Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean:[Les familles libres maximales d'un module ont-elles le meme cardinal?][lazarus1973] ./Mathlib/LinearAlgebra/Eigenspace/Basic.lean:* [Sheldon Axler, *Linear Algebra Done Right*][axler2015] ./Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean:* [Sheldon Axler, *Linear Algebra Done Right*][axler2015] ./Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean: des isomorphismes*][ribenboim1971] ./Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean:* [Djoković, D. Ž. *Epimorphisms of modules which must be isomorphisms*][djokovic1973] ./Mathlib/LinearAlgebra/FreeModule/StrongRankCondition.lean:* [Orzech, Morris. *Onto endomorphisms are isomorphisms*][orzech1971] ./Mathlib/LinearAlgebra/InvariantBasisNumber.lean:* [Djoković, D. Ž. *Epimorphisms of modules which must be isomorphisms*][djokovic1973] ./Mathlib/LinearAlgebra/InvariantBasisNumber.lean: *Épimorphismes de modules qui sont nécessairement des isomorphismes*][ribenboim1971] ./Mathlib/LinearAlgebra/InvariantBasisNumber.lean:* [Orzech, Morris. *Onto endomorphisms are isomorphisms*][orzech1971] ./Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean: * [M. Demazure, *SGA III, Expos\'{e} XXI, Don\'{e}es Radicielles*][demazure1970] ./Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean: * [N. Bourbaki, *Lie groups and {L}ie algebras. {C}hapters 4--6*][bourbaki1968] ./Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean: * [M. Demazure, *SGA III, Expos\'{e} XXI, Don\'{e}es Radicielles*][demazure1970] ./Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean: * [N. Bourbaki, *Lie groups and {L}ie algebras. {C}hapters 4--6*][bourbaki1968] ./Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean:* [*Algebra I*, Bourbaki : Chapter III, §4.7, example (2)][bourbaki1989] ./Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean:* [*Algebra I*, Bourbaki : Chapter III, §4.7, example (2)][bourbaki1989] ./Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean:* [A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term] ./Mathlib/Logic/Godel/GodelBetaFunction.lean:* [R. Kaye, *Models of Peano arithmetic*][kaye1991] ./Mathlib/MeasureTheory/Covering/Differentiation.lean:* [Herbert Federer, Geometric Measure Theory, Chapter 2.9][Federer1996] ./Mathlib/MeasureTheory/Decomposition/Exhaustion.lean:* [P. R. Halmos, *Measure theory*, 17.3 and 30.11][halmos1950measure] ./Mathlib/MeasureTheory/Function/Intersectivity.lean:`ℤᵐ`][bergelson1985] ./Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean:* [Walter Rudin, Real and Complex Analysis.][Rud87] ./Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean:[Rudin, *Real and Complex Analysis* (Theorem 2.24)][rudin2006real] ./Mathlib/MeasureTheory/Measure/FiniteMeasure.lean:* [Billingsley, *Convergence of probability measures*][billingsley1999] ./Mathlib/MeasureTheory/Measure/Haar/Unique.lean:[Halmos, Measure Theory][halmos1950measure] ./Mathlib/MeasureTheory/Measure/Hausdorff.lean:* [Herbert Federer, Geometric Measure Theory, Chapter 2.10][Federer1996] ./Mathlib/MeasureTheory/Measure/Portmanteau.lean:* [Billingsley, *Convergence of probability measures*][billingsley1999] ./Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean:* [Billingsley, *Convergence of probability measures*][billingsley1999] ./Mathlib/MeasureTheory/Measure/Regular.lean:[Billingsley, Convergence of Probability Measures][billingsley1999] ./Mathlib/MeasureTheory/Measure/Regular.lean:[Bogachev, Measure Theory, volume 2, Theorem 7.11.1][bogachev2007] ./Mathlib/MeasureTheory/Measure/SeparableMeasure.lean:* [D. L. Cohn, *Measure Theory*][cohn2013measure] ./Mathlib/ModelTheory/Fraisse.lean:- [W. Hodges, *A Shorter Model Theory*][Hodges97] ./Mathlib/NumberTheory/Bertrand.lean:* [M. Aigner and G. M. Ziegler _Proofs from THE BOOK_][aigner1999proofs] ./Mathlib/NumberTheory/Bertrand.lean:* [M. Carneiro, _Arithmetic in Metamath, Case Study: Bertrand's Postulate_][carneiro2015arithmetic] ./Mathlib/NumberTheory/Dioph.lean:* [M. Carneiro, _A Lean formalization of Matiyasevic's theorem_][carneiro2018matiyasevic] ./Mathlib/NumberTheory/Dioph.lean:* [M. Davis, _Hilbert's tenth problem is unsolvable_][MR317916] ./Mathlib/NumberTheory/FactorisationProperties.lean:* [R. W. Prielipp, *PERFECT NUMBERS, ABUNDANT NUMBERS, AND DEFICIENT NUMBERS*][Prielipp1970] ./Mathlib/NumberTheory/FunctionField.lean:* [D. Marcus, *Number Fields*][marcus1977number] ./Mathlib/NumberTheory/FunctionField.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/NumberTheory/FunctionField.lean:* [P. Samuel, *Algebraic Theory of Numbers*][samuel1970algebraic] ./Mathlib/NumberTheory/JacobiSum/Basic.lean: (Section 8.3)][IrelandRosen1990] ./Mathlib/NumberTheory/KummerDedekind.lean: * [J. Neukirch, *Algebraic Number Theory*][Neukirch1992] ./Mathlib/NumberTheory/MaricaSchoenheim.lean:[*Applications of the FKG Inequality and Its Relatives*, Graham][Graham1983] ./Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean:* [F. Diamond and J. Shurman, *A First Course in Modular Forms*][diamondshurman2005] ./Mathlib/NumberTheory/NumberField/AdeleRing.lean: * [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/NumberTheory/NumberField/Basic.lean:* [D. Marcus, *Number Fields*][marcus1977number] ./Mathlib/NumberTheory/NumberField/Basic.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/NumberTheory/NumberField/Basic.lean:* [P. Samuel, *Algebraic Theory of Numbers*][samuel1970algebraic] ./Mathlib/NumberTheory/NumberField/House.lean:* [D. Marcus, *Number Fields*][marcus1977number] ./Mathlib/NumberTheory/NumberField/House.lean:* [Hua, L.-K., *Introduction to number theory*][hua1982house] ./Mathlib/NumberTheory/Ostrowski.lean:* [J. W. S. Cassels, *Local fields*][cassels1986local] ./Mathlib/NumberTheory/Ostrowski.lean:* [K. Conrad, *Ostrowski for number fields*][conradnumbfield] ./Mathlib/NumberTheory/Ostrowski.lean:* [K. Conrad, *Ostrowski's Theorem for Q*][conradQ] ./Mathlib/NumberTheory/Padics/Hensel.lean:* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019] ./Mathlib/NumberTheory/Padics/MahlerBasis.lean: p-adic variable by polynomials*][bojanic74] ./Mathlib/NumberTheory/Padics/MahlerBasis.lean:* [P. Colmez, *Fonctions d'une variable p-adique*][colmez2010] ./Mathlib/NumberTheory/Padics/PadicIntegers.lean:* [F. Q. Gouvêa, *p-adic numbers*][gouvea1997] ./Mathlib/NumberTheory/Padics/PadicIntegers.lean:* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019] ./Mathlib/NumberTheory/Padics/PadicNorm.lean:* [F. Q. Gouvêa, *p-adic numbers*][gouvea1997] ./Mathlib/NumberTheory/Padics/PadicNorm.lean:* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019] ./Mathlib/NumberTheory/Padics/PadicNumbers.lean:* [F. Q. Gouvêa, *p-adic numbers*][gouvea1997] ./Mathlib/NumberTheory/Padics/PadicNumbers.lean:* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019] ./Mathlib/NumberTheory/Padics/PadicVal/Basic.lean:* [F. Q. Gouvêa, *p-adic numbers*][gouvea1997] ./Mathlib/NumberTheory/Padics/PadicVal/Basic.lean:* [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019] ./Mathlib/NumberTheory/Pell.lean: (Section 17.5)][IrelandRosen1990] ./Mathlib/NumberTheory/PellMatiyasevic.lean:* [M. Carneiro, _A Lean formalization of Matiyasevič's theorem_][carneiro2018matiyasevic] ./Mathlib/NumberTheory/PellMatiyasevic.lean:* [M. Davis, _Hilbert's tenth problem is unsolvable_][MR317916] ./Mathlib/Order/Birkhoff.lean:* [G. Birkhoff, *Rings of sets*][birkhoff1937] ./Mathlib/Order/BooleanAlgebra.lean:* [*Lattice Theory: Foundation*, George Grätzer][Gratzer2011] ./Mathlib/Order/BooleanAlgebra.lean:* [*Postulates for Boolean Algebras and Generalized Boolean Algebras*, M.H. Stone][Stone1935] ./Mathlib/Order/CompactlyGenerated/Basic.lean:- [G. Călugăreanu, *Lattice Concepts of Module Theory*][calugareanu] ./Mathlib/Order/Directed.lean:* [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980] ./Mathlib/Order/Filter/Basic.lean:* [N. Bourbaki, *General Topology*][bourbaki1966] ./Mathlib/Order/Filter/Defs.lean:* [N. Bourbaki, *General Topology*][bourbaki1966] ./Mathlib/Order/Grade.lean:* [Konrad Engel, *Sperner Theory*][engel1997] ./Mathlib/Order/Grade.lean:* [Richard Stanley, *Enumerative Combinatorics*][stanley2012] ./Mathlib/Order/ModularLattice.lean:* [Manfred Stern, *Semimodular lattices. {Theory} and applications*][stern2009] ./Mathlib/Order/OmegaCompletePartialOrder.lean: * [Chain-complete posets and directed sets with applications][markowsky1976] ./Mathlib/Order/OmegaCompletePartialOrder.lean: * [Recursive definitions of partial functions and their computations][cadiou1972] ./Mathlib/Order/OmegaCompletePartialOrder.lean: * [Semantics of Programming Languages: Structures and Techniques][gunter1992] ./Mathlib/Order/PrimeSeparator.lean:(1938)][Sto1938] ./Mathlib/Order/ScottContinuity.lean:* [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980] ./Mathlib/Order/WellFoundedSet.lean: * [Higman, *Ordering by Divisibility in Abstract Algebras*][Higman52] ./Mathlib/Probability/Martingale/Upcrossing.lean:We mostly follow the proof from [Kallenberg, *Foundations of modern probability*][kallenberg2021] ./Mathlib/RingTheory/Binomial.lean:* [J. Elliott, *Binomial rings, integer-valued polynomials, and λ-rings*][elliott2006binomial] ./Mathlib/RingTheory/DedekindDomain/AdicValuation.lean:* [G. J. Janusz, *Algebraic Number Fields*][janusz1996] ./Mathlib/RingTheory/DedekindDomain/AdicValuation.lean:* [J. Neukirch, *Algebraic Number Theory*][Neukirch1992] ./Mathlib/RingTheory/DedekindDomain/AdicValuation.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/RingTheory/DedekindDomain/Basic.lean:* [D. Marcus, *Number Fields*][marcus1977number] ./Mathlib/RingTheory/DedekindDomain/Basic.lean:* [J. Neukirch, *Algebraic Number Theory*][Neukirch1992] ./Mathlib/RingTheory/DedekindDomain/Basic.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/RingTheory/DedekindDomain/Dvr.lean:* [D. Marcus, *Number Fields*][marcus1977number] ./Mathlib/RingTheory/DedekindDomain/Dvr.lean:* [J. Neukirch, *Algebraic Number Theory*][Neukirch1992] ./Mathlib/RingTheory/DedekindDomain/Dvr.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/RingTheory/DedekindDomain/Ideal.lean:* [D. Marcus, *Number Fields*][marcus1977number] ./Mathlib/RingTheory/DedekindDomain/Ideal.lean:* [J. Neukirch, *Algebraic Number Theory*][Neukirch1992] ./Mathlib/RingTheory/DedekindDomain/Ideal.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean:* [D. Marcus, *Number Fields*][marcus1977number] ./Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean:* [J. Neukirch, *Algebraic Number Theory*][Neukirch1992] ./Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean:* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/RingTheory/DedekindDomain/SInteger.lean: * [D Marcus, *Number Fields*][marcus1977number] ./Mathlib/RingTheory/DedekindDomain/SInteger.lean: * [J Neukirch, *Algebraic Number Theory*][Neukirch1992] ./Mathlib/RingTheory/DedekindDomain/SInteger.lean: * [J W S Cassels, A Frölich, *Algebraic Number Theory*][cassels1967algebraic] ./Mathlib/RingTheory/Etale/Field.lean:- [B. Iversen, *Generic Local Structure of the Morphisms in Commutative Algebra*][iversen] ./Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean:* [Robin Hartshorne, *Algebraic Geometry*][Har77] ./Mathlib/RingTheory/HopfAlgebra.lean:* [C. Kassel, *Quantum Groups* (§III.3)][Kassel1995] ./Mathlib/RingTheory/LittleWedderburn.lean: [Chintala, Vineeth, *Sorry, the Nilpotents Are in the Center*][chintala2020] ./Mathlib/RingTheory/LittleWedderburn.lean: [Dolan, S. W., *A Proof of Jacobson's Theorem*][dolan1975] ./Mathlib/RingTheory/OreLocalization/Basic.lean:* [Zoran Škoda, *Noncommutative localization in noncommutative geometry*][skoda2006] ./Mathlib/RingTheory/OrzechProperty.lean:* [Djoković, D. Ž. *Epimorphisms of modules which must be isomorphisms*][djokovic1973] ./Mathlib/RingTheory/OrzechProperty.lean: *Épimorphismes de modules qui sont nécessairement des isomorphismes*][ribenboim1971] ./Mathlib/RingTheory/OrzechProperty.lean:* [Orzech, Morris. *Onto endomorphisms are isomorphisms*][orzech1971] ./Mathlib/RingTheory/Polynomial/Dickson.lean:* [R. Lidl, G. L. Mullen and G. Turnwald, _Dickson polynomials_][MR1237403] ./Mathlib/RingTheory/Smooth/Kaehler.lean:- [B. Iversen, *Generic Local Structure of the Morphisms in Commutative Algebra*][iversen] ./Mathlib/RingTheory/TensorProduct/Basic.lean:* [C. Kassel, *Quantum Groups* (§II.4)][Kassel1995] ./Mathlib/RingTheory/Unramified/Field.lean:- [B. Iversen, *Generic Local Structure of the Morphisms in Commutative Algebra*][iversen] ./Mathlib/RingTheory/Unramified/Finite.lean:- [B. Iversen, *Generic Local Structure of the Morphisms in Commutative Algebra*][iversen] ./Mathlib/RingTheory/WittVector/Basic.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Basic.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Compare.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Compare.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Defs.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Defs.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Frobenius.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Frobenius.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Identities.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Identities.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/InitTail.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/InitTail.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Isocrystal.lean:* [Theory of commutative formal groups over fields of finite characteristic][manin1963] ./Mathlib/RingTheory/WittVector/IsPoly.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/IsPoly.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/MulP.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/MulP.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/StructurePolynomial.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/StructurePolynomial.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Teichmuller.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Teichmuller.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Truncated.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Truncated.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/Verschiebung.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/Verschiebung.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/RingTheory/WittVector/WittPolynomial.lean:* [Commelin and Lewis, *Formalizing the Ring of Witt Vectors*][CL21] ./Mathlib/RingTheory/WittVector/WittPolynomial.lean:* [Hazewinkel, *Witt Vectors*][Haze09] ./Mathlib/SetTheory/Game/PGame.lean:* [Andreas Blass, *A game semantics for linear logic*][MR1167694] ./Mathlib/SetTheory/Game/PGame.lean:* [André Joyal, *Remarques sur la théorie des jeux à deux personnes*][joyal1997] ./Mathlib/SetTheory/Game/PGame.lean:* [Conway, *On numbers and games*][conway2001] ./Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean:* [F. Echenique, *A short and constructive proof of Tarski’s fixed-point theorem*][Echenique2005] ./Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean:* [P. Cousot & R. Cousot, *Constructive Versions of Tarski's Fixed Point Theorems*][Cousot1979] ./Mathlib/SetTheory/Surreal/Basic.lean:* [Conway, *On numbers and games*][Conway2001] ./Mathlib/SetTheory/Surreal/Basic.lean:* [Schleicher, Stoll, *An introduction to Conway's games and numbers*][SchleicherStoll] ./Mathlib/SetTheory/Surreal/Multiplication.lean:* [Conway, *On numbers and games*][Conway2001] ./Mathlib/SetTheory/Surreal/Multiplication.lean:* [Schleicher, Stoll, *An introduction to Conway's games and numbers*][SchleicherStoll] ./Mathlib/Topology/Algebra/FilterBasis.lean:* [N. Bourbaki, *General Topology*][bourbaki1966] ./Mathlib/Topology/Algebra/Module/StrongTopology.lean:* [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Topology/Algebra/Module/UniformConvergence.lean:* [N. Bourbaki, *General Topology, Chapter X*][bourbaki1966] ./Mathlib/Topology/Algebra/Module/UniformConvergence.lean:* [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Topology/Algebra/Module/WeakBilin.lean:* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] ./Mathlib/Topology/Algebra/Module/WeakDual.lean:* [H. H. Schaefer, *Topological Vector Spaces*][schaefer1966] ./Mathlib/Topology/Algebra/ProperAction/Basic.lean:* [N. Bourbaki, *General Topology*][bourbaki1966] ./Mathlib/Topology/Algebra/UniformConvergence.lean:* [N. Bourbaki, *General Topology, Chapter X*][bourbaki1966] ./Mathlib/Topology/Algebra/UniformConvergence.lean:* [N. Bourbaki, *Topological Vector Spaces*][bourbaki1987] ./Mathlib/Topology/Algebra/UniformGroup/Basic.lean:is itself complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b] ./Mathlib/Topology/Algebra/UniformGroup/Basic.lean:[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b] ./Mathlib/Topology/Algebra/UniformGroup/Basic.lean:subspaces are complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b] ./Mathlib/Topology/Basic.lean:* [I. M. James, *Topologies and Uniformities*][james1999] ./Mathlib/Topology/Basic.lean:* [N. Bourbaki, *General Topology*][bourbaki1966] ./Mathlib/Topology/CompletelyRegular.lean:* [Russell C. Walker, *The Stone-Čech Compactification*][russell1974] ./Mathlib/Topology/ExtremallyDisconnected.lean:[Gleason, *Projective topological spaces*][gleason1958] ./Mathlib/Topology/Homotopy/HSpaces.lean: Ann. of Math (2) 1951, 54, 425–505][serre1951] ./Mathlib/Topology/Maps/Proper/Basic.lean:* [N. Bourbaki, *General Topology*][bourbaki1966] ./Mathlib/Topology/MetricSpace/Dilation.lean:- [Marcel Berger, *Geometry*][berger1987] ./Mathlib/Topology/Order/Category/FrameAdjunction.lean:* [J. Picado and A. Pultr, Frames and Locales: topology without points][picado2011frames] ./Mathlib/Topology/Order/Lattice.lean:* [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980] ./Mathlib/Topology/Order/LawsonTopology.lean:* [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980] ./Mathlib/Topology/Order/LowerUpperTopology.lean:* [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980] ./Mathlib/Topology/Order/ScottTopology.lean:* [Gierz et al, *A Compendium of Continuous Lattices*][GierzEtAl1980] ./Mathlib/Topology/Order/ScottTopology.lean:* [Karner, *Continuous monoids and semirings*][Karner2004] ./Mathlib/Topology/Separation/Basic.lean:* [Willard's *General Topology*][zbMATH02107988] ./Mathlib/Topology/UniformSpace/AbsoluteValue.lean:* [N. Bourbaki, *Topologie générale*][bourbaki1966] ./Mathlib/Topology/UniformSpace/Ascoli.lean:* [N. Bourbaki, *General Topology, Chapter X*][bourbaki1966] ./Mathlib/Topology/UniformSpace/Basic.lean:* [I. M. James, *Topologies and Uniformities*][james1999] ./Mathlib/Topology/UniformSpace/Basic.lean:* [N. Bourbaki, *General Topology*][bourbaki1966] ./Mathlib/Topology/UniformSpace/CompareReals.lean:* [N. Bourbaki, *Topologie générale*][bourbaki1966] ./Mathlib/Topology/UniformSpace/Equicontinuity.lean:* [N. Bourbaki, *General Topology, Chapter X*][bourbaki1966] ./Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean:* [N. Bourbaki, *General Topology, Chapter X*][bourbaki1966]

Note:  References can appear in multiple places, so this list has expanded to 325 (compared to 148 unique) items.