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. [1]
[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.
[Bor94c] Francis Borceux, Handbook of Categorical Algebra: Volume 3, Sheaf Theory. 1994. [1]
[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. [1] [2] [3] [4]
[Bou87] N. Bourbaki, Topological vector spaces. Chapters 1–5. 1987. [1]
[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. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12]
[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.
[Cho94] Ching-Tsun Chou, A formal theory of undirected graphs in higher-order logic. Higher Order Logic Theorem Proving and Its Applications, 1994.
[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.
[DLM22] Frédéric Dupuis, Robert Lewis, Heather Macbeth, Formalized functional analysis with semilinear maps. 2022.
[DP02] B. Davey, H. Priestley, Introduction to lattices and order. 2002.
[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.
[Fre03] David Fremlin, Measure theory. Vol. 4. 2003.
[Fre10] David Fremlin, Measure theory. Vol. 2. 2010.
[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. [1]
[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. [1]
[Gra11] George Grätzer, Lattice Theory: Foundation. 2011. [1] [2]
[Gun92] Carl Gunter, Semantics of Programming Languages: Structures and Techniques. 1992. [1] [2] [3]
[HOS84] Harald Hanche-Olsen, Erling Størmer, Jordan operator algebras. Monogr. Stud. Math., 1984.
[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. [1]
[Hod97] Wilfrid Hodges, A Shorter Model Theory. 1997.
[Hof79] Douglas Hofstadter, Gödel, Escher, Bach: an eternal golden braid. 1979.
[How] Peter Howard, Second Order Elliptic PDE: The Lax-Milgram Theorem. M612: Partial Differential Equations, .
[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.
[JS86] André Joyal, Ross Street, Braided monoidal categories. 1986.
[Jam99] Ioan James, Topologies and uniformities. 1999. [1] [2]
[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.
[Kec95] Alexander Kechris, Classical descriptive set theory. 1995.
[Kle79] Steven Kleiman, Misconceptions about K_X. Enseign. Math. (2), 1979. [1]
[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. [1]
[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. [1]
[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. [1] [2] [3] [4] [5]
[Man63] Ju. Manin, Theory of commutative formal groups over fields of finite characteristic. Uspehi Mat. Nauk, 1963.
[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. [1]
[Nag78] Masayoshi Nagata, On Euclid algorithm. C. P. Ramanujam—a tribute, 1978. [1]
[Neu99] J. Neukirch, Algebraic number theory. 1999. [1] [2] [3] [4] [5]
[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.
[TZ12] Katrin Tent, Martin Ziegler, A Course in Model Theory. 2012.
[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. [1] [2] [3] [4]
[Zaa66] A. Zaanen, Lectures on "Riesz Spaces". 1966.
[Zor37] Max Zorn, On a theorem of Engel. Bull. Amer. Math. Soc., 1937.
[vdH01] Joris Hoeven, Operators on generalized power series. Illinois Journal of Mathematics, 2001. [1]
[vdW48] B. Waerden, Free products of groups. Amer. J. Math., 1948.