Update mer. 28 juin 2023 16:59:18 CEST

Changes

15 changed files (+14/-14)

• html/.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: 798c3985ff3075064f96be164dceb162 + config: dfa3c760a9c309561b2de03685612f6b tags: 645f666f9bcd5a90fca523b33c5a78b7
• html/C01_Introduction.html
  • @@ -347,7 +347,7 @@ Formal Mathematics.</p>
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C02_Basics.html
  • @@ -1416,7 +1416,7 @@ As you may have guessed, this theorem is called <code class="docutils literal no
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C03_Logic.html
  • @@ -1708,7 +1708,7 @@ but also abstracting over different types of convergence.</p>
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C04_Sets_and_Functions.html
  • @@ -1167,7 +1167,7 @@ and the proof uses the fact that <code class="docutils literal notranslate"><spa
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C05_Number_Theory.html
  • @@ -1158,7 +1158,7 @@ feat of formalization.</p>
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C06_Structures.html
  • @@ -1547,7 +1547,7 @@ the notions of being prime and being irreducible coincide.</p>
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C07_Hierarchies.html
  • @@ -986,7 +986,7 @@ to you.</p>
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C08_Topology.html
  • @@ -1214,7 +1214,7 @@ cover <code class="docutils literal notranslate"><span class="pre">s</span></cod
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C09_Differential_Calculus.html
  • @@ -454,7 +454,7 @@ see <code class="docutils literal notranslate"><span class="pre">HasFDerivWithin
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/C10_Integration_and_Measure_Theory.html
  • @@ -296,7 +296,7 @@ gives finite mass to compact sets, and give positive mass to open sets.</p>
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/genindex.html
  • @@ -533,7 +533,7 @@
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/index.html
  • @@ -166,7 +166,7 @@
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• html/search.html
  • @@ -103,7 +103,7 @@
    <hr/> <div role="contentinfo"> - <p>&#169; Copyright 2020, Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot.</p> + <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p> </div> Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
• mathematics_in_lean.pdf