1. Top
  2. mathematics_in_lean
  3. Files
  4. html
  5. index.html
mathematics_in_lean

My solutions for this book

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
  67. 67
  68. 68
  69. 69
  70. 70
  71. 71
  72. 72
  73. 73
  74. 74
  75. 75
  76. 76
  77. 77
  78. 78
  79. 79
  80. 80
  81. 81
  82. 82
  83. 83
  84. 84
  85. 85
  86. 86
  87. 87
  88. 88
  89. 89
  90. 90
  91. 91
  92. 92
  93. 93
  94. 94
  95. 95
  96. 96
  97. 97
  98. 98
  99. 99
  100. 100
  101. 101
  102. 102
  103. 103
  104. 104
  105. 105
  106. 106
  107. 107
  108. 108
  109. 109
  110. 110
  111. 111
  112. 112
  113. 113
  114. 114
  115. 115
  116. 116
  117. 117
  118. 118
  119. 119
  120. 120
  121. 121
  122. 122
  123. 123
  124. 124
  125. 125
  126. 126
  127. 127
  128. 128
  129. 129
  130. 130
  131. 131
  132. 132
  133. 133
  134. 134
  135. 135
  136. 136
  137. 137
  138. 138
  139. 139
  140. 140
  141. 141
  142. 142
  143. 143
  144. 144
  145. 145
  146. 146
  147. 147
  148. 148
  149. 149
  150. 150
  151. 151
  152. 152
  153. 153
  154. 154
  155. 155
  156. 156
  157. 157
  158. 158
  159. 159
  160. 160
  161. 161
  162. 162
  163. 163
  164. 164
  165. 165
  166. 166
  167. 167
  168. 168
  169. 169
  170. 170
  171. 171
  172. 172
  173. 173
  174. 174
  175. 175
  176. 176
  177. 177
  178. 178
  179. 179
  180. 180
  181. 181
  182. 182
  183. 183
  184. 184
  185. 185
  186. 186
  187. 187
  188. 188
  189. 189
  190. 190
  191. 191
  192. 192
  193. 193
  194. 194
  195. 195
  196. 196
  197. 197
  198. 198
  199. 199
  200. 200
  201. 201
  202. 202
  203. 203
  204. 204
  205. 205
  206. 206
  207. 207
  208. 208
  209. 209
  210. 210
  211. 211 


<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>Mathematics in Lean &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=e59714d7" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
      <script src="_static/jquery.js?v=5d32c60e"></script>
      <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
      <script src="_static/documentation_options.js?v=7048e04d"></script>
      <script src="_static/doctools.js?v=9bcbadda"></script>
      <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="1. Introduction" href="C01_Introduction.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="#" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="#">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="#" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active">Mathematics in Lean</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/index.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="mathematics-in-lean">
<h1>Mathematics in Lean<a class="headerlink" href="#mathematics-in-lean" title="Link to this heading">&#61633;</a></h1>
<div class="toctree-wrapper compound">
<ul>
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C01_Introduction.html#getting-started">1.1. Getting Started</a></li>
<li class="toctree-l2"><a class="reference internal" href="C01_Introduction.html#overview">1.2. Overview</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#calculating">2.1. Calculating</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#proving-identities-in-algebraic-structures">2.2. Proving Identities in Algebraic Structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#using-theorems-and-lemmas">2.3. Using Theorems and Lemmas</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#more-examples-using-apply-and-rw">2.4. More examples using apply and rw</a></li>
<li class="toctree-l2"><a class="reference internal" href="C02_Basics.html#proving-facts-about-algebraic-structures">2.5. Proving Facts about Algebraic Structures</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#implication-and-the-universal-quantifier">3.1. Implication and the Universal Quantifier</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#the-existential-quantifier">3.2. The Existential Quantifier</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#negation">3.3. Negation</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#conjunction-and-iff">3.4. Conjunction and Iff</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#disjunction">3.5. Disjunction</a></li>
<li class="toctree-l2"><a class="reference internal" href="C03_Logic.html#sequences-and-convergence">3.6. Sequences and Convergence</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C04_Sets_and_Functions.html#sets">4.1. Sets</a></li>
<li class="toctree-l2"><a class="reference internal" href="C04_Sets_and_Functions.html#functions">4.2. Functions</a></li>
<li class="toctree-l2"><a class="reference internal" href="C04_Sets_and_Functions.html#the-schroder-bernstein-theorem">4.3. The Schr&#246;der-Bernstein Theorem</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#irrational-roots">5.1. Irrational Roots</a></li>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#induction-and-recursion">5.2. Induction and Recursion</a></li>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#infinitely-many-primes">5.3. Infinitely Many Primes</a></li>
<li class="toctree-l2"><a class="reference internal" href="C05_Elementary_Number_Theory.html#more-induction">5.4. More Induction</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C06_Discrete_Mathematics.html#finsets-and-fintypes">6.1. Finsets and Fintypes</a></li>
<li class="toctree-l2"><a class="reference internal" href="C06_Discrete_Mathematics.html#counting-arguments">6.2. Counting Arguments</a></li>
<li class="toctree-l2"><a class="reference internal" href="C06_Discrete_Mathematics.html#inductively-defined-types">6.3. Inductively Defined Types</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C07_Structures.html#defining-structures">7.1. Defining structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="C07_Structures.html#algebraic-structures">7.2. Algebraic Structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="C07_Structures.html#building-the-gaussian-integers">7.3. Building the Gaussian Integers</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C08_Hierarchies.html#basics">8.1. Basics</a></li>
<li class="toctree-l2"><a class="reference internal" href="C08_Hierarchies.html#morphisms">8.2. Morphisms</a></li>
<li class="toctree-l2"><a class="reference internal" href="C08_Hierarchies.html#sub-objects">8.3. Sub-objects</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C09_Groups_and_Rings.html#monoids-and-groups">9.1. Monoids and Groups</a></li>
<li class="toctree-l2"><a class="reference internal" href="C09_Groups_and_Rings.html#rings">9.2. Rings</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#vector-spaces-and-linear-maps">10.1. Vector spaces and linear maps</a></li>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#subspaces-and-quotients">10.2. Subspaces and quotients</a></li>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#endomorphisms">10.3. Endomorphisms</a></li>
<li class="toctree-l2"><a class="reference internal" href="C10_Linear_Algebra.html#matrices-bases-and-dimension">10.4. Matrices, bases and dimension</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C11_Topology.html#filters">11.1. Filters</a></li>
<li class="toctree-l2"><a class="reference internal" href="C11_Topology.html#metric-spaces">11.2. Metric spaces</a></li>
<li class="toctree-l2"><a class="reference internal" href="C11_Topology.html#topological-spaces">11.3. Topological spaces</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C12_Differential_Calculus.html#elementary-differential-calculus">12.1. Elementary Differential Calculus</a></li>
<li class="toctree-l2"><a class="reference internal" href="C12_Differential_Calculus.html#differential-calculus-in-normed-spaces">12.2. Differential Calculus in Normed Spaces</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html#elementary-integration">13.1. Elementary Integration</a></li>
<li class="toctree-l2"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html#measure-theory">13.2. Measure Theory</a></li>
<li class="toctree-l2"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html#integration">13.3. Integration</a></li>
</ul>
</li>
</ul>
</div>
<div class="toctree-wrapper compound">
</div>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C01_Introduction.html" class="btn btn-neutral float-right" title="1. Introduction" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>