Update lun. 04 déc. 2023 09:48:19 EST

leanprover-community · Dec 4, 2023 · 067e331 · 067e331
1 parent 60d59f5
commit 067e331
Show file tree

Hide file tree

Showing 25 changed files with 1,181 additions and 1,241 deletions.
diff --git a/.buildinfo b/.buildinfo
@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 9821478498fa33697c987b601aae688f
+config: 803b947a09f3db5a52c6c529e3761a53
 tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/C01_Introduction.html b/C01_Introduction.html
@@ -1,8 +1,7 @@
 <!DOCTYPE html>
 <html class="writer-html5" lang="en" >
 <head>
-  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
-
+  <meta charset="utf-8" />
   <meta name="viewport" content="width=device-width, initial-scale=1.0" />
   <title>1. Introduction &mdash; Mathematics in Lean 0.1 documentation</title>
       <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
@@ -16,7 +15,6 @@
         <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
         <script src="_static/jquery.js"></script>
         <script src="_static/underscore.js"></script>
-        <script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
         <script src="_static/doctools.js"></script>
     <script src="_static/js/theme.js"></script>
     <link rel="index" title="Index" href="genindex.html" />
@@ -85,10 +83,10 @@
           <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
            <div itemprop="articleBody">
 
-  <section id="introduction">
-<span id="id1"></span><h1><span class="section-number">1. </span>Introduction<a class="headerlink" href="#introduction" title="Permalink to this heading">&#61633;</a></h1>
-<section id="getting-started">
-<h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink" href="#getting-started" title="Permalink to this heading">&#61633;</a></h2>
+  <div class="section" id="introduction">
+<span id="id1"></span><h1><span class="section-number">1. </span>Introduction<a class="headerlink" href="#introduction" title="Permalink to this headline">&#61633;</a></h1>
+<div class="section" id="getting-started">
+<h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink" href="#getting-started" title="Permalink to this headline">&#61633;</a></h2>
 <p>The goal of this book is to teach you to formalize mathematics using the
 Lean 4 interactive proof assistant.
 It assumes that you know some mathematics, but it does not require much.
@@ -173,9 +171,9 @@ <h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink
 the relevant skills, feel free to move on.
 You can always compare your solutions to the ones in the <code class="docutils literal notranslate"><span class="pre">solutions</span></code>
 folder associated with each section.</p>
-</section>
-<section id="overview">
-<h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href="#overview" title="Permalink to this heading">&#61633;</a></h2>
+</div>
+<div class="section" id="overview">
+<h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href="#overview" title="Permalink to this headline">&#61633;</a></h2>
 <p>Put simply, Lean is a tool for building complex expressions in a formal language
 known as <em>dependent type theory</em>.</p>
 <p id="index-0">Every expression has a <em>type</em>, and you can use the <cite>#check</cite> command to
@@ -347,8 +345,8 @@ <h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href=
 Bartosz Piotrowski, Nicolas Rolland, Guilherme Silva, Floris van Doorn, and Eric Wieser.
 Our work has been partially supported by the Hoskinson Center for
 Formal Mathematics.</p>
-</section>
-</section>
+</div>
+</div>
 
 
            </div>

diff --git a/C02_Basics.html b/C02_Basics.html
@@ -1,8 +1,7 @@
 <!DOCTYPE html>
 <html class="writer-html5" lang="en" >
 <head>
-  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
-
+  <meta charset="utf-8" />
   <meta name="viewport" content="width=device-width, initial-scale=1.0" />
   <title>2. Basics &mdash; Mathematics in Lean 0.1 documentation</title>
       <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
@@ -16,7 +15,6 @@
         <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
         <script src="_static/jquery.js"></script>
         <script src="_static/underscore.js"></script>
-        <script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
         <script src="_static/doctools.js"></script>
         <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
     <script src="_static/js/theme.js"></script>
@@ -89,14 +87,14 @@
           <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
            <div itemprop="articleBody">
 
-  <section id="basics">
-<span id="id1"></span><h1><span class="section-number">2. </span>Basics<a class="headerlink" href="#basics" title="Permalink to this heading">&#61633;</a></h1>
+  <div class="section" id="basics">
+<span id="id1"></span><h1><span class="section-number">2. </span>Basics<a class="headerlink" href="#basics" title="Permalink to this headline">&#61633;</a></h1>
 <p>This chapter is designed to introduce you to the nuts and
 bolts of mathematical reasoning in Lean: calculating,
 applying lemmas and theorems,
 and reasoning about generic structures.</p>
-<section id="calculating">
-<h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" href="#calculating" title="Permalink to this heading">&#61633;</a></h2>
+<div class="section" id="calculating">
+<h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" href="#calculating" title="Permalink to this headline">&#61633;</a></h2>
 <p>We generally learn to carry out mathematical calculations
 without thinking of them as proofs.
 But when we justify each step in a calculation,
@@ -385,9 +383,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
   <span class="n">rw</span> <span class="o">[</span><span class="n">add_mul</span><span class="o">]</span>
 </pre></div>
 </div>
-</section>
-<section id="proving-identities-in-algebraic-structures">
-<span id="id2"></span><h2><span class="section-number">2.2. </span>Proving Identities in Algebraic Structures<a class="headerlink" href="#proving-identities-in-algebraic-structures" title="Permalink to this heading">&#61633;</a></h2>
+</div>
+<div class="section" id="proving-identities-in-algebraic-structures">
+<span id="id2"></span><h2><span class="section-number">2.2. </span>Proving Identities in Algebraic Structures<a class="headerlink" href="#proving-identities-in-algebraic-structures" title="Permalink to this headline">&#61633;</a></h2>
 <p id="index-7">Mathematically, a ring consists of a collection of objects,
 <span class="math notranslate nohighlight">\(R\)</span>, operations <span class="math notranslate nohighlight">\(+\)</span> <span class="math notranslate nohighlight">\(\times\)</span>, and constants <span class="math notranslate nohighlight">\(0\)</span>
 and <span class="math notranslate nohighlight">\(1\)</span>, and an operation <span class="math notranslate nohighlight">\(x \mapsto -x\)</span> such that:</p>
@@ -705,9 +703,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 <cite>noncomm_ring</cite> and <cite>ring</cite>. This is partly for historical reasons,
 but also for the convenience of using a shorter name for the
 tactic that deals with commutative rings, since it is used more often.</p>
-</section>
-<section id="using-theorems-and-lemmas">
-<span id="id3"></span><h2><span class="section-number">2.3. </span>Using Theorems and Lemmas<a class="headerlink" href="#using-theorems-and-lemmas" title="Permalink to this heading">&#61633;</a></h2>
+</div>
+<div class="section" id="using-theorems-and-lemmas">
+<span id="id3"></span><h2><span class="section-number">2.3. </span>Using Theorems and Lemmas<a class="headerlink" href="#using-theorems-and-lemmas" title="Permalink to this headline">&#61633;</a></h2>
 <p id="index-16">Rewriting is great for proving equations,
 but what about other sorts of theorems?
 For example, how can we prove an inequality,
@@ -974,9 +972,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 </div>
 <p>If you managed to solve this, congratulations!
 You are well on your way to becoming a master formalizer.</p>
-</section>
-<section id="more-examples-using-apply-and-rw">
-<span id="more-on-order-and-divisibility"></span><h2><span class="section-number">2.4. </span>More examples using apply and rw<a class="headerlink" href="#more-examples-using-apply-and-rw" title="Permalink to this heading">&#61633;</a></h2>
+</div>
+<div class="section" id="more-examples-using-apply-and-rw">
+<span id="more-on-order-and-divisibility"></span><h2><span class="section-number">2.4. </span>More examples using apply and rw<a class="headerlink" href="#more-examples-using-apply-and-rw" title="Permalink to this headline">&#61633;</a></h2>
 <p id="index-21">The <code class="docutils literal notranslate"><span class="pre">min</span></code> function on the real numbers is uniquely characterized
 by the following three facts:</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="o">(</span><span class="n">min_le_left</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">min</span> <span class="n">a</span> <span class="n">b</span> <span class="bp">&#8804;</span> <span class="n">a</span><span class="o">)</span>
@@ -1176,9 +1174,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 the one specifically for the natural numbers.
 You can use <code class="docutils literal notranslate"><span class="pre">_root_.dvd_antisymm</span></code> to specify the generic one;
 either one will work.</p>
-</section>
-<section id="proving-facts-about-algebraic-structures">
-<span id="id4"></span><h2><span class="section-number">2.5. </span>Proving Facts about Algebraic Structures<a class="headerlink" href="#proving-facts-about-algebraic-structures" title="Permalink to this heading">&#61633;</a></h2>
+</div>
+<div class="section" id="proving-facts-about-algebraic-structures">
+<span id="id4"></span><h2><span class="section-number">2.5. </span>Proving Facts about Algebraic Structures<a class="headerlink" href="#proving-facts-about-algebraic-structures" title="Permalink to this headline">&#61633;</a></h2>
 <p id="index-27">In <a class="reference internal" href="#proving-identities-in-algebraic-structures"><span class="std std-numref">Section 2.2</span></a>,
 we saw that many common identities governing the real numbers hold
 in more general classes of algebraic structures,
@@ -1391,8 +1389,8 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 </div>
 <p>We recommend making use of the theorem <code class="docutils literal notranslate"><span class="pre">nonneg_of_mul_nonneg_left</span></code>.
 As you may have guessed, this theorem is called <code class="docutils literal notranslate"><span class="pre">dist_nonneg</span></code> in Mathlib.</p>
-</section>
-</section>
+</div>
+</div>
 
 
            </div>