References

Works cited in mathlib are collected on this page. This is generated from the BibTeX file docs/references.bib (view on GitHub).

• [ACH19] Jeremy Avigad, Mario Carneiro, Simon Hudon, Data Types as Quotients of Polynomial Functors. 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, 2019.
• [AL19] Benedikt Ahrens, Peter Lumsdaine, Displayed Categories. Logical Methods in Computer Science, 2019.
• [AM69] M. Atiyah, I. Macdonald, Introduction to commutative algebra. 1969.
• [AdMK17] Jeremy Avigad, Leonardo Moura, Soonho Kong, Theorem Proving in Lean. 2017.
• [Alu16] Paolo Aluffi, Algebra: Chapter 0. 2016.
• [Axl15] Sheldon Axler, Linear algebra done right. 3rd ed.. Undergraduate Texts Math., 2015.
• [BD96] Ilya Beylin, Peter Dybjer, Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. Types for Proofs and Programs, 1996.
• [Ban] Banasiak, Banach Lattices in Applications. .
• [Bea04] Richard Beals, Analysis. An introduction. 2004.
• [Bel64] J. Bell, On the Einstein Podolsky Rosen paradox. Phys. Phys. Fiz., 1964.
• [Ber12] S. Bernstein, Démonstration du théorème de Weierstrass fondée sur le calcul des probabilités. Comm. Kharkov Math. Soc., 1912.
• [Bil99] Patrick Billingsley, Convergence of probability measures. 1999.
• [Bir42] Garrett Birkhoff, Lattice, ordered groups. Ann. of Math. (2), 1942.
• [Bla92] Andreas Blass, A game semantics for linear logic. Ann. Pure Appl. Logic, 1992.
• [Bor94a] Francis Borceux, Handbook of Categorical Algebra: Volume 1, Basic Category Theory. 1994.
• [Bor94b] Francis Borceux, Handbook of Categorical Algebra: Volume 2, Categories and Structures. 1994.
• [Bou02] Nicolas Bourbaki, Lie groups and Lie algebras. Chapters 4–6. 2002.
• [Bou05] Nicolas Bourbaki, Lie groups and Lie algebras. Chapters 7–9. 2005.
• [Bou66] Nicolas Bourbaki, Elements of mathematics. General topology. Part 1. 1966.
• [Bou90] N. Bourbaki, Algebra. II. Chapters 4–7. 1990.
• [Bou98] Nicolas Bourbaki, Lie groups and Lie algebras. Chapters 1–3. 1998.
• [CF67] John Cassels, Albrecht Frölich, Algebraic number theory: proceedings of an instructional conference. 1967.
• [CHSH69] John Clauser, Michael Horne, Abner Shimony, Richard Holt, Proposed experiment to test local hidden-variable theories. Phys. Rev. Lett., 1969.
• [CL21] Johan Commelin, Robert Lewis, Formalizing the Ring of Witt Vectors. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021.
• [CM72] Jean Cadiou, Zohar Manna, Recursive definitions of partial functions and their computations. ACM SIGACT News, 1972. [1]
• [Cal00] Grigore Cǎlugǎreanu, Lattice Concepts of Module Theory. 2000. [1]
• [Car18] Mario Carneiro, A Lean formalization of Matiyasevič's theorem. 2018.
• [Car19] Mario Carneiro, Formalizing Computability Theory via Partial Recursive Functions. 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, 2019.
• [Con01] J. Conway, On numbers and games. 2001.
• [Cs80] B. Cirel son, Quantum generalizations of Bell's inequality. Lett. Math. Phys., 1980.
• [DG70] Michel Demazure, Pierre Gabriel, Groupes algébriques. Tome I: Géométrie algébrique, généralités, groupes commutatifs. 1970.
• [Dav73] Martin Davis, Hilbert's tenth problem is unsolvable. Amer. Math. Monthly, 1973.
• [Del75] P. Deligne, Courbes elliptiques: formulaire d'après J. Tate. Modular functions of one variable, IV (Proc. Internat. Summer School, Univ. Antwerp, Antwerp, 1972), 1975.
• [Dyc92] Roy Dyckhoff, Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 1992. [1]
• [EW17] Manfred Einsiedler, Thomas Ward, Functional Analysis, Spectral Theory, and Applications. 2017.
• [FL94] Zoltán Füredi, Peter Loeb, On the best constant for the Besicovitch covering theorem. Proc. Am. Math. Soc., 1994.
• [FLST20] Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel, Quotients of Bounded Natural Functors. Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, 2020.
• [FR92] Roger Fenn, Colin Rourke, Racks and links in codimension two. Journal of Knot Theory and its Ramifications, 1992.
• [Fed96] Herbert Federer, Geometric Measure Theory. 1996.
• [Fuc63] L. Fuchs, Partially ordered algebraic systems. 1963.
• [GHK+80] Gerhard Gierz, Karl Hofmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, Dana Scott, A compendium of continuous lattices. 1980.
• [GMM] Alena Gusakov, Bhavik Mehta, Kyle Miller, Formalizing Hall's Marriage Theorem in Lean. .
• [GO09] Jeremy Gibbons, BRUNO Oliveira, The essence of the Iterator pattern. Journal of Functional Programming, 2009. [1]
• [GQ11] J. Gallier, J. Quaintance, Notes on Differential Geometry and Lie Groups. 2011.
• [Ghy87] Étienne Ghys, Groupes d'homéomorphismes du cercle et cohomologie bornée. Contemporary Mathematics, 1987.
• [Gor55] Russel Gordon, The integrals of Lebesgue, Denjoy, Perron, and Henstock. 1955.
• [Gou97] Fernando Gouvêa, p-adic numbers. 1997.
• [Gra11] George Grätzer, Lattice Theory: Foundation. 2011. [1] [2]
• [Gun92] Carl Gunter, Semantics of Programming Languages: Structures and Techniques. 1992. [1] [2] [3]
• [HW91] John Hubbard, Beverly West, Differential Equations: A Dynamical Systems Approach. 1991.
• [HWHBS08] GH Hardy, EM Wright, Roger Heath-Brown, Joseph Silverman, An Introduction to the Theory of Numbers. 2008.
• [Hal35] P. Hall, On Representatives of Subsets. Journal of the London Mathematical Society, 1935.
• [Hal50a] Paul Halmos, Measure theory. 1950.
• [Hal50b] Paul Halmos, Measure theory. 1950.
• [Hal66] James Halpern, Bases in vector spaces and the axiom of choice. Proc. Amer. Math. Soc., 1966.
• [Har77] Robin Hartshorne, Algebraic geometry. 1977.
• [Haz09] Michiel Hazewinkel, Witt vectors. Part 1. Handbook of Algebra, 2009.
• [Hib75] Jean-Jacques Hiblot, Des anneaux euclidiens dont le plus petit algorithme n'est pas à valeurs finies. C. R. Acad. Sci. Paris Sér. A-B, 1975. [1]
• [Hig52] Graham Higman, Ordering by Divisibility in Abstract Algebras. Proceedings of the London Mathematical Society, 1952.
• [Hof79] Douglas Hofstadter, Gödel, Escher, Bach: an eternal golden braid. 1979.
• [Hun02] Craig Huneke, The Friendship Theorem. The American Mathematical Monthly, 2002.
• [HvD19] Jesse Han, Floris Doorn, A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. 10th International Conference on Interactive Theorem Proving (ITP 2019), 2019.
• [HvD20] Jesse Han, Floris Doorn, A formal proof of the independence of the continuum hypothesis. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
• [Jam99] Ioan James, Topologies and uniformities. 1999.
• [Joh02] Peter Johnstone, Sketches of an Elephant – A Topos Theory Compendium. 2002.
• [Joy77] André Joyal, Remarques sur la théorie des jeux à deux personnes. Gazette des Sciences Mathematiques du Québec, 1977.
• [Joy82] David Joyce, A classifying invariant of knots, the knot quandle. Journal of Pure and Applied Algebra, 1982.
• [KM85] Nicholas Katz, Barry Mazur, Arithmetic moduli of elliptic curves. 1985.
• [LMT93] R. Lidl, G. Mullen, G. Turnwald, Dickson polynomials. 1993.
• [Laz73] Michel Lazarus, Les familles libres maximales d'un module ont-elles le meme cardinal?. Pub. Sem. Math. Rennes, 1973.
• [Lew19] Robert Lewis, A Formal Proof of Hensel's Lemma over the p-adic Integers. Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019.
• [Lur18] Jacob Lurie, Spectral Algebraic Geometry. last updated 2018.
• [MM92] Saunders MacLane, Ieke Moerdijk, Sheaves in geometry and logic: A first introduction to topos theory. 1992.
• [MN91] Peter Meyer-Nieberg, Banach lattices. 1991.
• [MS77] Daniel Marcus, Emanuele Sacco, Number fields. 1977.
• [Mar76] George Markowsky, Chain-complete posets and directed sets with applications. Algebra Universalis, 1976. [1]
• [McB96] Conor McBride, Inverting inductively defined relations in LEGO. International Workshop on Types for Proofs and Programs, 1996. [1]
• [Mir06] F. Miraglia, An Introduction to Partially Ordered Structures and Sheaves. 2006.
• [Mot49] Th. Motzkin, The Euclidean algorithm. Bull. Amer. Math. Soc., 1949. [1]
• [NW63] C. Nash-Williams, On well-quasi-ordering finite trees. Mathematical Proceedings of the Cambridge Philosophical Society, 1963.
• [Nag78] Masayoshi Nagata, On Euclid algorithm. C. P. Ramanujam—a tribute, 1978. [1]
• [Neu99] J. Neukirch, Algebraic number theory. 1999.
• [Oro18] Greg Orosi, A simple derivation of Faulhaber's formula. Appl. Math. E-Notes, 2018.
• [PES66] P. Erdös, V. Sós, On a problem of graph theory. Studia Sci. Math., 1966.
• [Phi40] Ralph Phillips, Integration in a convex linear topological space. Trans. Amer. Math. Soc., 1940.
• [Pon20] Lionel Ponton, Roots of Chebyshev polynomials: a purely algebraic approach. 2020.
• [Pos17] Jürgen Pöschel, On the Siegel-Sternberg linearization theorem. 2017.
• [Rie17] Emily Riehl, Category theory in context. 2017.
• [Rud69] Mary Rudin, A new proof that metric spaces are paracompact. Proc. Amer. Math. Soc., 1969.
• [Rud87] Walter Rudin, Real and Complex Analysis. 1987.
• [SS] Dierk Schleicher, Michael Stoll, An introduction to Conway's games and numbers. .
• [Sam67] Pierre Samuel, Théorie algébrique des nombres. 1967.
• [Sch11] Peter Scholze, Perfectoid spaces. 2011.
• [Sch66] H.H. Schaefer, Topological Vector Spaces. 1966.
• [Sel67] G. Seligman, Modular Lie algebras. 1967.
• [Ser87] Jean-Pierre Serre, Complex semisimple Lie algebras. 1987.
• [Sim11] Barry Simon, Convexity: An Analytic Viewpoint. 2011.
• [Soa87] Robert Soare, Recursively enumerable sets and degrees. 1987.
• [Sto35] M. Stone, Postulates for Boolean Algebras and Generalized Boolean Algebras. American Journal of Mathematics, 1935. [1] [2]
• [Sto79] A. Stone, Inverse limits of compact spaces. General Topology Appl., 1979.
• [Tao10] Terence Tao, An Epsilon of Room, I: Real Analysis: Pages from Year Three of a Mathematical Blog. 2010.
• [Vai03] Jussi Väisälä, A Proof of the Mazur-Ulam Theorem. The American Mathematical Monthly, 2003.
• [Wal18] H.S. Wall, Analytic Theory of Continued Fractions. 2018.
• [Was04] Larry Wasserman, All Of Statistics: A Concise Course in Statistical Inference. 2004.
• [Wed19] Torsten Wedhorn, Adic Spaces. 2019.
• [Zaa66] A. Zaanen, Lectures on "Riesz Spaces". 1966.
• [vdH01] Joris Hoeven, Operators on generalized power series. Illinois Journal of Mathematics, 2001.
• [vdW48] B. Waerden, Free products of groups. Amer. J. Math., 1948.