CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

| Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Project: Xena
Views: 18536
License: APACHE
Tweet
Share
Share
1
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

2
%                                                                     %

3
% This is a database of documents referenced in mathlib file headers. %

4
%                                                                     %

5
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

6


7
@article {MR1167694,

8
    AUTHOR = {Blass, Andreas},

9
     TITLE = {A game semantics for linear logic},

10
   JOURNAL = {Ann. Pure Appl. Logic},

11
  FJOURNAL = {Annals of Pure and Applied Logic},

12
    VOLUME = {56},

13
      YEAR = {1992},

14
    NUMBER = {1-3},

15
     PAGES = {183--220},

16
      ISSN = {0168-0072},

17
   MRCLASS = {03B70 (68Q55)},

18
  MRNUMBER = {1167694},

19
MRREVIEWER = {Fangmin Song},

20
       DOI = {10.1016/0168-0072(92)90073-9},

21
       URL = {https://doi.org/10.1016/0168-0072(92)90073-9},

22
}

23


24
@book {bourbaki1966,

25
    AUTHOR = {Bourbaki, Nicolas},

26
     TITLE = {Elements of mathematics. {G}eneral topology. {P}art 1},

27
 PUBLISHER = {Hermann, Paris; Addison-Wesley Publishing Co., Reading,

28
              Mass.-London-Don Mills, Ont.},

29
      YEAR = {1966},

30
     PAGES = {vii+437},

31
   MRCLASS = {54.00 (00.00)},

32
  MRNUMBER = {0205210},

33
}

34


35
@book {bourbaki1975,

36
    AUTHOR = {Bourbaki, Nicolas},

37
     TITLE = {Lie groups and {L}ie algebras. {C}hapters 1--3},

38
    SERIES = {Elements of Mathematics (Berlin)},

39
      NOTE = {Translated from the French,

40
              Reprint of the 1989 English translation},

41
 PUBLISHER = {Springer-Verlag, Berlin},

42
      YEAR = {1998},

43
     PAGES = {xviii+450},

44
      ISBN = {3-540-64242-0},

45
   MRCLASS = {17Bxx (00A05 22Exx)},

46
  MRNUMBER = {1728312},

47
}

48


49
@book {conway2001,

50
    AUTHOR = {Conway, J. H.},

51
     TITLE = {On numbers and games},

52
   EDITION = {Second},

53
 PUBLISHER = {A K Peters, Ltd., Natick, MA},

54
      YEAR = {2001},

55
     PAGES = {xii+242},

56
      ISBN = {1-56881-127-6},

57
   MRCLASS = {00A08 (05-01 91A05)},

58
  MRNUMBER = {1803095},

59
}

60


61
@book {gouvea1997,

62
    AUTHOR = {Gouv\^{e}a, Fernando Q.},

63
     TITLE = {{$p$}-adic numbers},

64
    SERIES = {Universitext},

65
   EDITION = {Second},

66
      NOTE = {An introduction},

67
 PUBLISHER = {Springer-Verlag, Berlin},

68
      YEAR = {1997},

69
     PAGES = {vi+298},

70
      ISBN = {3-540-62911-4},

71
   MRCLASS = {11S80 (11-01 12J25)},

72
  MRNUMBER = {1488696},

73
       DOI = {10.1007/978-3-642-59058-0},

74
       URL = {https://doi.org/10.1007/978-3-642-59058-0},

75
}

76


77
@book {james1999,

78
    AUTHOR = {James, Ioan},

79
     TITLE = {Topologies and uniformities},

80
    SERIES = {Springer Undergraduate Mathematics Series},

81
      NOTE = {Revised version of {{\i}t Topological and uniform spaces}

82
              [Springer, New York, 1987;  MR0884154 (89b:54001)]},

83
 PUBLISHER = {Springer-Verlag London, Ltd., London},

84
      YEAR = {1999},

85
     PAGES = {xvi+230},

86
      ISBN = {1-85233-061-9},

87
   MRCLASS = {54-01 (54A05 54E15)},

88
  MRNUMBER = {1687407},

89
MRREVIEWER = {Hans-Peter A. K\"{u}nzi},

90
       DOI = {10.1007/978-1-4471-3994-2},

91
       URL = {https://doi.org/10.1007/978-1-4471-3994-2},

92
}

93


94
@article {joyal1977,

95
 author = {André Joyal},

96
 title = {Remarques sur la théorie des jeux à deux personnes},

97
 journal = {Gazette des Sciences Mathematiques du Québec},

98
 volume = {1},

99
 number = {4},

100
 pages = {46--52},

101
 year = {1977},

102
 note = {(English translation at https://bosker.files.wordpress.com/2010/12/joyal-games.pdf)}

103
}

104


105
@inproceedings{lewis2019,

106
 author = {Lewis, Robert Y.},

107
 title = {A Formal Proof of {H}ensel's Lemma over the {$p$}-adic Integers},

108
 booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},

109
 series = {CPP 2019},

110
 year = {2019},

111
 isbn = {978-1-4503-6222-1},

112
 location = {Cascais, Portugal},

113
 pages = {15--26},

114
 numpages = {12},

115
 url = {http://doi.acm.org/10.1145/3293880.3294089},

116
 doi = {10.1145/3293880.3294089},

117
 acmid = {3294089},

118
 publisher = {ACM},

119
 address = {New York, NY, USA},

120
 keywords = {Hensel's lemma, Lean, formal proof, p-adic},

121
}

122


123
@book {riehl2017,

124
   AUTHOR = {Riehl, Emily},

125
    TITLE = {Category theory in context},

126
PUBLISHER = {Dover Publications},

127
     YEAR = {2017},

128
     ISBN = {048680903X},

129
      URL = {http://www.math.jhu.edu/~eriehl/context.pdf},

130
}

131


132
@book{wall2018analytic,

133
  title={Analytic Theory of Continued Fractions},

134
  author={Wall, H.S.},

135
  isbn={9780486830445},

136
  series={Dover Books on Mathematics},

137
  year={2018},

138
  publisher={Dover Publications}

139
}

140


141
@article{ahrens2017,

142
 author = {Benedikt Ahrens and Peter LeFanu Lumsdaine},

143
   year = {2019},

144
  title = {Displayed Categories},

145
journal = {Logical Methods in Computer Science},

146
 volume = {15},

147
  issue = {1},

148
    doi = {10.23638/LMCS-15(1:20)2019},

149
}

150


151
@Book{HubbardWest-ode,

152
author = {John H. Hubbard and Beverly H. West},

153
title = {Differential Equations: A Dynamical Systems Approach},

154
subtitle = {Ordinary Differential Equations},

155
year = {1991},

156
publisher = {Springer},

157
location = {New York},

158
volume = {5},

159
isbn = {978-1-4612-8693-6},

160
doi = {10.1007/978-1-4612-4192-8},

161
pages = {XX, 350},

162
}

163


164