Update C01_Introduction.html (#14)

Changes

2 changed files (+4/-4)

• html/C01_Introduction.html
  • @@ -310,7 +310,7 @@ powerful and ever-growing library, <em>Mathlib</em>.
    As a result, we can show you how to use some of the mathematical objects and theorems in the library, and some of the very useful tactics. - This book is not meant to be used as an complete overview of the library; + This book is not meant to be used as a complete overview of the library; the <a class="reference external" href="https://leanprover-community.github.io/">community</a> web pages contain extensive documentation. Rather, our goal is to introduce you to the style of thinking that
  • @@ -379,4 +379,4 @@ Formal Mathematics.</p>
    </script> </body> - </html> + </html>
• html/C02_Basics.html
  • @@ -372,7 +372,7 @@ but we will see in the next section that it can be used
    for calculations on structures other than the real numbers. It can be imported explicitly with the command <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">Mathlib.Tactic</span></code>. - We will see there are similar tactics for other common kind of algebraic + We will see there are similar tactics for other common kinds of algebraic structures.</p> <p>There is a variation of <code class="docutils literal notranslate"><span class="pre">rw</span></code> called <code class="docutils literal notranslate"><span class="pre">nth_rewrite</span></code> that allows you to replace only particular instances of an expression in the goal. Possible matches are enumerated starting with 1,
  • @@ -1423,4 +1423,4 @@ As you may have guessed, this theorem is called <code class="docutils literal no
    </script> </body> - </html> + </html>