Update ven. 25 avril 2025 05:14:52 CEST

Author: PatrickMassot

C02_Basics.html

@@ -1363,7 +1363,7 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 with a partial order on the carrier
 satisfying additional axioms that say that the ring operations
 are compatible with the order:</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">StrictOrderedRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">PartialOrder</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsStrictOrderedRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
 <span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span>
 
 <span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_le_add_left</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>

C03_Logic.html

@@ -289,7 +289,7 @@
 and real numbers are all instances.
 So if we prove the theorem <code class="docutils literal notranslate"><span class="pre">fnUb_add</span></code> at that level of generality,
 it will apply in all these instances.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">OrderedCancelAddCommMonoid</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommMonoid</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">PartialOrder</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsOrderedCancelAddMonoid</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
 
 <span class="k">#check</span><span class="w"> </span><span class="n">add_le_add</span>
 

C04_Sets_and_Functions.html

@@ -891,22 +891,19 @@
 <span class="math notranslate nohighlight">\(g\)</span> in <span class="math notranslate nohighlight">\(\alpha\)</span>.
 On that image, the inverse of <span class="math notranslate nohighlight">\(g\)</span> is defined and is a bijection
 with <span class="math notranslate nohighlight">\(\beta\)</span>.</p>
-<a class="reference internal image-reference" href="_images/schroeder_bernstein1.png"><img alt="the Schr&#246;der Bernstein theorem" class="align-center" src="_images/schroeder_bernstein1.png" style="height: 150px;" />
-</a>
+<a class="reference internal image-reference" href="_images/schroeder_bernstein1.png"><img alt="the Schr&#246;der Bernstein theorem" class="align-center" src="_images/schroeder_bernstein1.png" style="height: 150px;" /></a>
 <p>The problem is that the bijection does not include the shaded region
 in the diagram, which is nonempty if <span class="math notranslate nohighlight">\(g\)</span> is not surjective.
 Alternatively, we can use <span class="math notranslate nohighlight">\(f\)</span> to map all of
 <span class="math notranslate nohighlight">\(\alpha\)</span> to <span class="math notranslate nohighlight">\(\beta\)</span>,
 but in that case the problem is that if <span class="math notranslate nohighlight">\(f\)</span> is not surjective,
 it will miss some elements of <span class="math notranslate nohighlight">\(\beta\)</span>.</p>
-<a class="reference internal image-reference" href="_images/schroeder_bernstein2.png"><img alt="the Schr&#246;der Bernstein theorem" class="align-center" src="_images/schroeder_bernstein2.png" style="height: 150px;" />
-</a>
+<a class="reference internal image-reference" href="_images/schroeder_bernstein2.png"><img alt="the Schr&#246;der Bernstein theorem" class="align-center" src="_images/schroeder_bernstein2.png" style="height: 150px;" /></a>
 <p>But now consider the composition <span class="math notranslate nohighlight">\(g \circ f\)</span> from <span class="math notranslate nohighlight">\(\alpha\)</span> to
 itself. Because the composition is injective, it forms a bijection between
 <span class="math notranslate nohighlight">\(\alpha\)</span> and its image, yielding a scaled-down copy of <span class="math notranslate nohighlight">\(\alpha\)</span>
 inside itself.</p>
-<a class="reference internal image-reference" href="_images/schroeder_bernstein3.png"><img alt="the Schr&#246;der Bernstein theorem" class="align-center" src="_images/schroeder_bernstein3.png" style="height: 150px;" />
-</a>
+<a class="reference internal image-reference" href="_images/schroeder_bernstein3.png"><img alt="the Schr&#246;der Bernstein theorem" class="align-center" src="_images/schroeder_bernstein3.png" style="height: 150px;" /></a>
 <p>This composition maps the inner shaded ring to yet another such
 set, which we can think of as an even smaller concentric shaded ring,
 and so on.

C06_Structures.html

@@ -1237,7 +1237,7 @@
 <span class="w">  </span><span class="n">Int.emod_nonneg</span><span class="w"> </span><span class="n">a</span>
 
 <span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="bp">|</span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="o">:=</span>
-<span class="w">  </span><span class="n">Int.emod_lt</span><span class="w"> </span><span class="n">a</span>
+<span class="w">  </span><span class="n">Int.emod_lt_abs</span><span class="w"> </span><span class="n">a</span>
 </pre></div>
 </div>
 <p>In an arbitrary ring, an element <span class="math notranslate nohighlight">\(a\)</span> is said to be a <em>unit</em> if it divides
@@ -1353,8 +1353,8 @@
 <p>We will use the fact that <span class="math notranslate nohighlight">\(x^2 + y^2\)</span> is equal to zero if and only if
 <span class="math notranslate nohighlight">\(x\)</span> and <span class="math notranslate nohighlight">\(y\)</span> are both zero. As an exercise, we ask you to prove
 that this holds in any ordered ring.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sq_add_sq_eq_zero</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">LinearOrderedRing</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
-<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">sq_add_sq_eq_zero</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">LinearOrder</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsStrictOrderedRing</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>
+<span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
 <span class="w">  </span><span class="gr">sorry</span>
 </pre></div>
 </div>
@@ -1510,7 +1510,7 @@
 <span class="w">    </span><span class="n">quotient</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
 <span class="w">    </span><span class="n">remainder</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">&#183;</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="bp">&#183;</span><span class="o">)</span>
 <span class="w">    </span><span class="n">quotient_mul_add_remainder_eq</span><span class="w"> </span><span class="o">:=</span>
-<span class="w">      </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="bp">;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mod_def</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">]</span><span class="w"> </span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>
+<span class="w">      </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mod_def</span><span class="o">,</span><span class="w"> </span><span class="n">add_comm</span><span class="o">]</span><span class="w"> </span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>
 <span class="w">    </span><span class="n">quotient_zero</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="kd">by</span>
 <span class="w">      </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">div_def</span><span class="o">,</span><span class="w"> </span><span class="n">norm</span><span class="o">,</span><span class="w"> </span><span class="n">Int.div&#39;</span><span class="o">]</span>
 <span class="w">      </span><span class="n">rfl</span>