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.
[AE72] Erik Alfsen, Edward Effros, Structure in real Banach spaces. I and II. Ann. Math. (2), 1972.
[AL19] Benedikt Ahrens, Peter Lumsdaine, Displayed Categories. Logical Methods in Computer Science, 2019. [1]
[AM69] M. Atiyah, I. Macdonald, Introduction to commutative algebra. 1969.
[AS03] Erik Alfsen, Frederic Shultz, Geometry of state spaces of operator algebras. 2003.
[AZ99] Martin Aigner, Günter Ziegler, Proofs from THE BOOK. Berlin. Germany, 1999.
[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.
[BGR84] S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis : A Systematic Approach to Rigid Analytic Geometry. 1984.
[BS13] M. Brodmann, R. Sharp, Local cohomology. 2013.
[BV04] Stephen Boyd, Lieven Vandenberghe, Convex Optimization. 2004.
[Ban] Banasiak, Banach Lattices in Applications. .
[Bea04] Richard Beals, Analysis. An introduction. 2004.
[Beh79] Ehrhard Behrends, M-structure and the Banach-Stone theorem. Lect. Notes Math., 1979.
[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.
[Ber87] Marcel Berger, Geometry I. 1987.
[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.
[Bol86] Béla Bollobás, Combinatorics: Set Systems, Hypergraphs, Families of Vectors, and Combinatorial Probability. 1986.
[Bor94a] Francis Borceux, Handbook of Categorical Algebra: Volume 1, Basic Category Theory. 1994. [1] [2]
[Bor94b] Francis Borceux, Handbook of Categorical Algebra: Volume 2, Categories and Structures. 1994. [1] [2] [3] [4]
[Bor94c] Francis Borceux, Handbook of Categorical Algebra: Volume 3, Sheaf Theory. 1994. [1] [2]
[Bou02] Nicolas Bourbaki, Lie groups and Lie algebras. Chapters 4–6. 2002.
[Bou05] Nicolas Bourbaki, Lie groups and Lie algebras. Chapters 7–9. 2005.
[Bou07] Nicolas Bourbaki, Algèbre. Chapitre IX. 2007.
[Bou66a] Nicolas Bourbaki, Elements of mathematics. General topology. Part 1. 1966. [1] [2] [3] [4] [5] [6] [7]
[Bou66b] Nicolas Bourbaki, Elements of mathematics. General topology. Part 2. 1966. [1] [2] [3] [4]
[Bou87] N. Bourbaki, Topological vector spaces. Chapters 1–5. 1987. [1] [2] [3] [4] [5]
[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öhlich, Algebraic number theory. Proceedings of an instructional conference organized by the London Mathematical Society (a NATO Advanced Study Institute) with the support of the International Mathematical Union, 1967.
[CGRP14] Miguel Cabrera García, Ángel Rodríguez Palacios, Non-associative normed algebras. Volume 1. The Vidav-Palmer and Gelfand-Naimark theorems. Encycl. Math. Appl., 2014.
[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.
[CLOShea97] David Cox, John Little, Donal O'Shea, Ideals, varieties, and algorithms - an introduction to computational algebraic geometry and commutative algebra (2. ed.). 1997. [1]
[CLW93] Aurelio Carboni, Stephen Lack, R.F.C. Walters, Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 1993.
[CM72] Jean Cadiou, Zohar Manna, Recursive definitions of partial functions and their computations. ACM SIGACT News, 1972. [1]
[CMP17] Alissa Crans, Sujoy Mukherjee, Józef Przytycki, On homology of associative shelves. J. Homotopy Relat. Struct., 2017.
[Cal00] Grigore Cǎlugǎreanu, Lattice Concepts of Module Theory. 2000. [1] [2] [3] [4]
[Car15] Mario Carneiro, Arithmetic in Metamath, Case Study: Bertrand's Postulate. arXiv preprint arXiv:1503.02349, 2015.
[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.
[Cas50] J. Cassels, Some metrical theorems in Diophantine approximation. I. Proc. Cambridge Philos. Soc., 1950.
[Cho94] Ching-Tsun Chou, A formal theory of undirected graphs in higher-order logic. Higher Order Logic Theorem Proving and Its Applications, 1994.
[Chu12] Cho-Ho Chu, Jordan structures in geometry and analysis. Camb. Tracts Math., 2012.
[Cla] Pete Clark, Geometry of Numbers with Applications to Number Theory. .
[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.
[DM22] Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean. 13th International Conference on Interactive Theorem Proving (ITP 2022), 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.
[Dol58] Albrecht Dold, Homology of symmetric products and other functors of complexes. Ann. of Math. (2), 1958.
[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.
[Eis95] David Eisenbud, Commutative algebra. 1995.
[Eng97] Konrad Engel, Sperner theory. 1997.
[Ete81] Nasrollah Etemadi, An elementary proof of the strong law of large numbers. Z. Wahrsch. Verw. Gebiete, 1981.
[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.
[Fre64] Peter Freyd, Abelian categories. 1964.
[Fri05] Yaakov Friedman, Physical applications of homogeneous balls. With the assistance of Tzvi Scarr. Prog. Math. Phys., 2005.
[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. [1]
[GJ09] Paul Goerss, John Jardine, Simplicial homotopy theory. 2009.
[GM] B. Gärtner, J. Matousek, Cone Programming. .
[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]
[GZ67] P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory. 1967.
[Gal61] Patrick Gallagher, Approximation by reduced fractions. J. Math. Soc. Japan, 1961.
[Ghy87] Étienne Ghys, Groupes d'homéomorphismes du cercle et cohomologie bornée. Contemporary Mathematics, 1987.
[Gle58] Andrew Gleason, Projective topological spaces. Illinois J. Math., 1958.
[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]
[Gri16] D. Grinberg, The Clifford algebra and the Chevalley map- a computational approach (summary version 1). 2016.
[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.
[HWW93] Peter Harmand, Dirk Werner, Wend Werner, M-ideals in Banach spaces and Banach algebras. Lect. Notes Math., 1993.
[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.
[Har67] Robin Hartshorne, Local cohomology. 1967.
[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]
[Hoc] Mel Hochster, Local cohomology. .
[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.
[IKR16] Zur Izhakian, Manfred Knebusch, Louis Rowen, Supertropical quadratic forms I. Journal of Pure and Applied Algebra, 2016.
[ILL+07] Srikanth Iyengar, Graham Leuschke, Anton Leykin, Claudia Miller, Ezra Miller, Anurag Singh, Uli Walther, Twenty-four hours of local cohomology. 2007.
[IR90] Kenneth Ireland, Michael Rosen, A classical introduction to modern number theory. 1990.
[Ior03] Radu Iordănescu, Jordan structures in geometry and physics. With an appendix on Jordan structures in analysis. 2003.
[JS86] André Joyal, Ross Street, Braided monoidal categories. 1986.
[Jac56] Nathan Jacobson, Structure of rings. 1956.
[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.
[JvN35] P. Jordan, J. Neumann, On inner products in linear, metric spaces. Ann. Math., 1935.
[KM20] Dimitris Koukoulopoulos, James Maynard, On the Duffin-Schaeffer conjecture. Ann. of Math. (2), 2020.
[KM85] Nicholas Katz, Barry Mazur, Arithmetic moduli of elliptic curves. 1985.
[KV53] J. Kelley, R. Vaught, The positive cone in Banach algebras. Trans. Am. Math. Soc., 1953. [1] [2]
[Kal21] Olav Kallenberg, Foundations of modern probability. 2021.
[Kec95] Alexander Kechris, Classical descriptive set theory. 1995.
[Kle66] D. Kleitman, Families of non-disjoint subsets. J. Comb. Theory, 1966.
[Kle79] Steven Kleiman, Misconceptions about K_X. Enseign. Math. (2), 1979.
[Koz94] D. Kozen, A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation, 1994. [1]
[LMT93] R. Lidl, G. Mullen, G. Turnwald, Dickson polynomials. 1993.
[LS04] S. Lack, P. Sobociński, Adhesive categories. Foundations of Software Science and Computation Structures, FoSSaCS '04, 2004.
[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.
[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.
[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]
[McC04] Kevin McCrimmon, A taste of Jordan algebras. Universitext, 2004.
[Mel11] Sergey Melikhov, Metrizable uniform spaces. 2011.
[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.
[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.
[Pet14] G. Petridis, The Plünnecke-Ruzsa inequality: an overview. Combinatorial and additive number theory. Selected papers based on the presentations at the conferences CANT 2011 and 2012, New York, NY, USA, May 2011 and May 2012, 2014.
[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. .
[Sal18] David Salwinski, Euler's sine product formula: an elementary proof. College Math. J., 2018.
[Sam67] Pierre Samuel, Théorie algébrique des nombres. 1967.
[Sch11] Peter Scholze, Perfectoid spaces. 2011.
[Sch66] H.H. Schaefer, Topological Vector Spaces. 1966. [1] [2] [3]
[Sel67] G. Seligman, Modular Lie algebras. 1967.
[Ser51] Jean-Pierre Serre, Homologie singulière des espaces fibrés. Applications. Ann. of Math. (2), 1951.
[Ser87] Jean-Pierre Serre, Complex semisimple Lie algebras. 1987.
[Sil09] Joseph Silverman, The Arithmetic of Elliptic Curves. 2009.
[Sim11] Barry Simon, Convexity: An Analytic Viewpoint. 2011.
[Sko06] Zoran Škoda, Noncommutative localization in noncommutative geometry. London Math. Soc. Lecture Note Series, 2006.
[Soa87] Robert Soare, Recursively enumerable sets and degrees. 1987.
[Sta12] Richard Stanley, Enumerative combinatorics. 2012.
[Ste09] Manfred Stern, Semimodular lattices. Theory and applications. 2009. [1]
[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.
[TV06] Terence Tao, Van Vu, Additive combinatorics. 2006.
[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.
[Toc] Shigenori Tochiori, Considering the Proof of "There is a Prime between n and 2n". .
[Upm87] Harald Upmeier, Jordan algebras in analysis, operator theory, and quantum mechanics. Reg. Conf. Ser. Math., 1987.
[Vai03] Jussi Väisälä, A Proof of the Mazur-Ulam Theorem. The American Mathematical Monthly, 2003.
[Vak] Ravi Vakil, The Rising Sea: Foundations Of Algebraic Geometry Notes. .
[WG] Emo Welzl, Bernd Gärtner, Cone Programming. .
[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]
[Wei80] Joachim Weidmann, Linear operators in Hilbert spaces. 1980.
[Zaa66] A. Zaanen, Lectures on "Riesz Spaces". 1966.
[Zor37] Max Zorn, On a theorem of Engel. Bull. Amer. Math. Soc., 1937.
[dMKA+15] Leonardo Moura, Soonho Kong, Jeremy Avigad, Floris Doorn, Jakob Raumer, The Lean Theorem Prover (System Description). Automated Deduction - CADE-25, 2015.
[mC20] The Community, The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
[vdH01] Joris Hoeven, Operators on generalized power series. Illinois Journal of Mathematics, 2001.
[vdW48] B. Waerden, Free products of groups. Amer. J. Math., 1948.