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. [1] [2] [3] [4] [5] [6] [7] [8]
[AE72] Erik Alfsen, Edward Effros, Structure in real Banach spaces. I and II. Ann. Math. (2), 1972. [1]
[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. [1]
[AZ99] Martin Aigner, Günter Ziegler, Proofs from THE BOOK. Berlin. Germany, 1999. [1]
[AdMK17] Jeremy Avigad, Leonardo Moura, Soonho Kong, Theorem Proving in Lean. 2017.
[Alu16] Paolo Aluffi, Algebra: Chapter 0. 2016. [1]
[Axl15] Sheldon Axler, Linear algebra done right. 3rd ed.. Undergraduate Texts Math., 2015. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10]
[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. [1] [2]
[BV04] Stephen Boyd, Lieven Vandenberghe, Convex Optimization. 2004. [1]
[Ban] Banasiak, Banach Lattices in Applications. . [1]
[Bea04] Richard Beals, Analysis. An introduction. 2004.
[Beh79] Ehrhard Behrends, M-structure and the Banach-Stone theorem. Lect. Notes Math., 1979. [1]
[Bel64] J. Bell, On the Einstein Podolsky Rosen paradox. Phys. Phys. Fiz., 1964. [1]
[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. [1] [2]
[Bir42] Garrett Birkhoff, Lattice, ordered groups. Ann. of Math. (2), 1942. [1] [2] [3]
[Bla92] Andreas Blass, A game semantics for linear logic. Ann. Pure Appl. Logic, 1992. [1]
[Bor94a] Francis Borceux, Handbook of Categorical Algebra: Volume 1, Basic Category Theory. 1994. [1] [2] [3]
[Bor94b] Francis Borceux, Handbook of Categorical Algebra: Volume 2, Categories and Structures. 1994. [1] [2] [3] [4] [5] [6] [7]
[Bor94c] Francis Borceux, Handbook of Categorical Algebra: Volume 3, Sheaf Theory. 1994. [1] [2] [3]
[Bou02] Nicolas Bourbaki, Lie groups and Lie algebras. Chapters 4–6. 2002. [1] [2] [3] [4] [5]
[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] [5] [6] [7]
[Bou87] N. Bourbaki, Topological vector spaces. Chapters 1–5. 1987. [1] [2] [3] [4] [5]
[Bou90] N. Bourbaki, Algebra. II. Chapters 4–7. 1990. [1]
[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]
[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. [1] [2]
[CHSH69] John Clauser, Michael Horne, Abner Shimony, Richard Holt, Proposed experiment to test local hidden-variable theories. Phys. Rev. Lett., 1969. [1]
[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. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13]
[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]
[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]
[Car15] Mario Carneiro, Arithmetic in Metamath, Case Study: Bertrand's Postulate. arXiv preprint arXiv:1503.02349, 2015. [1]
[Car18] Mario Carneiro, A Lean formalization of Matiyasevič's theorem. 2018. [1] [2]
[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. [1] [2] [3] [4]
[Cho94] Ching-Tsun Chou, A formal theory of undirected graphs in higher-order logic. Higher Order Logic Theorem Proving and Its Applications, 1994. [1]
[Chu12] Cho-Ho Chu, Jordan structures in geometry and analysis. Camb. Tracts Math., 2012. [1]
[Con01] J. Conway, On numbers and games. 2001. [1] [2] [3]
[Cs80] B. Cirel son, Quantum generalizations of Bell's inequality. Lett. Math. Phys., 1980. [1]
[DG70] Michel Demazure, Pierre Gabriel, Groupes algébriques. Tome I: Géométrie algébrique, généralités, groupes commutatifs. 1970. [1]
[DLM22] Frédéric Dupuis, Robert Lewis, Heather Macbeth, Formalized functional analysis with semilinear maps. 2022. [1] [2] [3]
[DP02] B. Davey, H. Priestley, Introduction to lattices and order. 2002. [1] [2]
[Dav73] Martin Davis, Hilbert's tenth problem is unsolvable. Amer. Math. Monthly, 1973. [1] [2]
[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. [1]
[Dol58] Albrecht Dold, Homology of symmetric products and other functors of complexes. Ann. of Math. (2), 1958. [1]
[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. [1]
[Eng97] Konrad Engel, Sperner theory. 1997. [1] [2]
[Ete81] Nasrollah Etemadi, An elementary proof of the strong law of large numbers. Z. Wahrsch. Verw. Gebiete, 1981. [1]
[FL94] Zoltán Füredi, Peter Loeb, On the best constant for the Besicovitch covering theorem. Proc. Am. Math. Soc., 1994. [1]
[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. [1]
[Fed96] Herbert Federer, Geometric Measure Theory. 1996. [1] [2] [3]
[Fre03] David Fremlin, Measure theory. Vol. 4. 2003.
[Fre10] David Fremlin, Measure theory. Vol. 2. 2010. [1] [2]
[Fre64] Peter Freyd, Abelian categories. 1964. [1]
[Fri05] Yaakov Friedman, Physical applications of homogeneous balls. With the assistance of Tzvi Scarr. Prog. Math. Phys., 2005. [1]
[Fuc63] L. Fuchs, Partially ordered algebraic systems. 1963. [1] [2]
[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. [1] [2] [3]
[GMM] Alena Gusakov, Bhavik Mehta, Kyle Miller, Formalizing Hall's Marriage Theorem in Lean. . [1]
[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. [1]
[Ghy87] Étienne Ghys, Groupes d'homéomorphismes du cercle et cohomologie bornée. Contemporary Mathematics, 1987. [1] [2] [3] [4] [5] [6] [7]
[Gor55] Russel Gordon, The integrals of Lebesgue, Denjoy, Perron, and Henstock. 1955. [1] [2]
[Gou97] Fernando Gouvêa, p-adic numbers. 1997. [1] [2] [3] [4]
[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. [1] [2]
[HW91] John Hubbard, Beverly West, Differential Equations: A Dynamical Systems Approach. 1991. [1]
[HWHBS08] GH Hardy, EM Wright, Roger Heath-Brown, Joseph Silverman, An Introduction to the Theory of Numbers. 2008. [1] [2] [3]
[HWW93] Peter Harmand, Dirk Werner, Wend Werner, M-ideals in Banach spaces and Banach algebras. Lect. Notes Math., 1993. [1]
[Hal35] P. Hall, On Representatives of Subsets. Journal of the London Mathematical Society, 1935. [1]
[Hal50a] Paul Halmos, Measure theory. 1950. [1]
[Hal50b] Paul Halmos, Measure theory. 1950.
[Hal66] James Halpern, Bases in vector spaces and the axiom of choice. Proc. Amer. Math. Soc., 1966. [1]
[Har77] Robin Hartshorne, Algebraic geometry. 1977. [1] [2] [3] [4] [5]
[Haz09] Michiel Hazewinkel, Witt vectors. Part 1. Handbook of Algebra, 2009. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16]
[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. [1]
[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, . [1]
[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. [1] [2] [3] [4]
[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. [1] [2] [3] [4]
[IKR16] Zur Izhakian, Manfred Knebusch, Louis Rowen, Supertropical quadratic forms I. Journal of Pure and Applied Algebra, 2016.
[Ior03] Radu Iordănescu, Jordan structures in geometry and physics. With an appendix on Jordan structures in analysis. 2003. [1]
[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. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] [19] [20] [21] [22]
[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. [1] [2]
[KM85] Nicholas Katz, Barry Mazur, Arithmetic moduli of elliptic curves. 1985. [1]
[Kal21] Olav Kallenberg, Foundations of modern probability. 2021. [1]
[Kec95] Alexander Kechris, Classical descriptive set theory. 1995.
[Kle66] D. Kleitman, Families of non-disjoint subsets. J. Comb. Theory, 1966. [1] [2] [3]
[Kle79] Steven Kleiman, Misconceptions about K_X. Enseign. Math. (2), 1979. [1]
[LMT93] R. Lidl, G. Mullen, G. Turnwald, Dickson polynomials. 1993. [1]
[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] [2] [3] [4] [5] [6]
[Lur18] Jacob Lurie, Spectral Algebraic Geometry. last updated 2018. [1]
[MM92] Saunders MacLane, Ieke Moerdijk, Sheaves in geometry and logic: A first introduction to topos theory. 1992. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] [19] [20] [21] [22] [23] [24] [25] [26] [27] [28] [29] [30] [31] [32] [33] [34] [35] [36] [37] [38] [39] [40]
[MN91] Peter Meyer-Nieberg, Banach lattices. 1991. [1]
[MS77] Daniel Marcus, Emanuele Sacco, Number fields. 1977. [1] [2] [3] [4] [5] [6]
[Man63] Ju. Manin, Theory of commutative formal groups over fields of finite characteristic. Uspehi Mat. Nauk, 1963. [1]
[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. [1] [2]
[Mel11] Sergey Melikhov, Metrizable uniform spaces. 2011. [1]
[Mir06] F. Miraglia, An Introduction to Partially Ordered Structures and Sheaves. 2006. [1]
[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] [6]
[Oro18] Greg Orosi, A simple derivation of Faulhaber's formula. Appl. Math. E-Notes, 2018. [1]
[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. [1]
[Pos17] Jürgen Pöschel, On the Siegel-Sternberg linearization theorem. 2017. [1]
[Rie17] Emily Riehl, Category theory in context. 2017. [1] [2] [3] [4] [5] [6] [7] [8] [9] [10]
[Rud69] Mary Rudin, A new proof that metric spaces are paracompact. Proc. Amer. Math. Soc., 1969. [1] [2]
[Rud87] Walter Rudin, Real and Complex Analysis. 1987. [1] [2]
[SS] Dierk Schleicher, Michael Stoll, An introduction to Conway's games and numbers. . [1]
[Sam67] Pierre Samuel, Théorie algébrique des nombres. 1967.
[Sch11] Peter Scholze, Perfectoid spaces. 2011. [1]
[Sch66] H.H. Schaefer, Topological Vector Spaces. 1966. [1] [2] [3] [4] [5] [6]
[Sel67] G. Seligman, Modular Lie algebras. 1967.
[Ser87] Jean-Pierre Serre, Complex semisimple Lie algebras. 1987.
[Sim11] Barry Simon, Convexity: An Analytic Viewpoint. 2011. [1] [2] [3]
[Sko06] Zoran Škoda, Noncommutative localization in noncommutative geometry. London Math. Soc. Lecture Note Series, 2006. [1]
[Soa87] Robert Soare, Recursively enumerable sets and degrees. 1987. [1]
[Sta12] Richard Stanley, Enumerative combinatorics. 2012. [1] [2]
[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. [1]
[TZ12] Katrin Tent, Martin Ziegler, A Course in Model Theory. 2012. [1]
[Tao10] Terence Tao, An Epsilon of Room, I: Real Analysis: Pages from Year Three of a Mathematical Blog. 2010. [1]
[Toc] Shigenori Tochiori, Considering the Proof of "There is a Prime between n and 2n". . [1]
[Upm87] Harald Upmeier, Jordan algebras in analysis, operator theory, and quantum mechanics. Reg. Conf. Ser. Math., 1987. [1]
[Vai03] Jussi Väisälä, A Proof of the Mazur-Ulam Theorem. The American Mathematical Monthly, 2003. [1]
[WG] Emo Welzl, Bernd Gärtner, Cone Programming. . [1]
[Wal18] H.S. Wall, Analytic Theory of Continued Fractions. 2018. [1] [2]
[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. [1]
[Zaa66] A. Zaanen, Lectures on "Riesz Spaces". 1966. [1]
[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. [1]