Update jeu. 22 août 2024 23:04:15 CEST

C05_Elementary_Number_Theory.html

@@ -800,7 +800,7 @@
 <span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">mgt2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">two_le</span><span class="w"> </span><span class="n">this</span><span class="w"> </span><span class="n">mne1</span>
 <span class="w">  </span><span class="n">by_cases</span><span class="w"> </span><span class="n">mp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m.Prime</span>
 <span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">mp</span>
-<span class="w">  </span><span class="bp">.</span><span class="w"> </span><span class="n">rcases</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">mltn</span><span class="w"> </span><span class="n">mgt2</span><span class="w"> </span><span class="n">mp</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
+<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">rcases</span><span class="w"> </span><span class="n">ih</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">mltn</span><span class="w"> </span><span class="n">mgt2</span><span class="w"> </span><span class="n">mp</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span><span class="o">,</span><span class="w"> </span><span class="n">pdvd</span><span class="o">&#10217;</span>
 <span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">p</span><span class="o">,</span><span class="w"> </span><span class="n">pp</span>
 <span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">pdvd.trans</span><span class="w"> </span><span class="n">mdvdn</span>
 </pre></div>

C06_Structures.html

@@ -1481,7 +1481,7 @@
 <span class="kd">theorem</span><span class="w"> </span><span class="n">natAbs_norm_mod_lt</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">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
 <span class="w">    </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">%</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="bp">.</span><span class="n">norm.natAbs</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y.norm.natAbs</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
 <span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">Int.ofNat_lt</span><span class="bp">.</span><span class="mi">1</span>
-<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">Int.coe_natAbs</span><span class="o">,</span><span class="w"> </span><span class="n">abs_of_nonneg</span><span class="o">,</span><span class="w"> </span><span class="n">norm_nonneg</span><span class="o">]</span>
+<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">Int.natCast_natAbs</span><span class="o">,</span><span class="w"> </span><span class="n">abs_of_nonneg</span><span class="o">,</span><span class="w"> </span><span class="n">norm_nonneg</span><span class="o">]</span>
 <span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">norm_mod_lt</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">hy</span>
 </pre></div>
 </div>
@@ -1525,7 +1525,7 @@
 <p>An immediate payoff is that we now know that, in the Gaussian integers,
 the notions of being prime and being irreducible coincide.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaussInt</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Irreducible</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">Prime</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
-<span class="w">  </span><span class="n">PrincipalIdealRing.irreducible_iff_prime</span>
+<span class="w">  </span><span class="n">irreducible_iff_prime</span>
 </pre></div>
 </div>
 </section>

C09_Topology.html

@@ -717,12 +717,12 @@ <h3><span class="section-number">9.2.3. </span>Compactness<a class="headerlink"
 <span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">X</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCompact</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hs&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">s.Nonempty</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">f</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">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span>
 <span class="w">      </span><span class="o">(</span><span class="n">hfs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContinuousOn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
 <span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">f</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">hs.exists_forall_le</span><span class="w"> </span><span class="n">hs&#39;</span><span class="w"> </span><span class="n">hfs</span>
+<span class="w">  </span><span class="n">hs.exists_isMinOn</span><span class="w"> </span><span class="n">hs&#39;</span><span class="w"> </span><span class="n">hfs</span>
 
 <span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">X</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCompact</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hs&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">s.Nonempty</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">f</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">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span>
 <span class="w">      </span><span class="o">(</span><span class="n">hfs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContinuousOn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
 <span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
-<span class="w">  </span><span class="n">hs.exists_forall_ge</span><span class="w"> </span><span class="n">hs&#39;</span><span class="w"> </span><span class="n">hfs</span>
+<span class="w">  </span><span class="n">hs.exists_isMaxOn</span><span class="w"> </span><span class="n">hs&#39;</span><span class="w"> </span><span class="n">hfs</span>
 
 <span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">X</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCompact</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsClosed</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span>
 <span class="w">  </span><span class="n">hs.isClosed</span>
@@ -788,7 +788,7 @@ <h3><span class="section-number">9.2.5. </span>Completeness<a class="headerlink"
 <p>We&#8217;ll practice using this definition by proving a convenient criterion which is a special case of a
 criterion appearing in Mathlib. This is also a good opportunity to practice using big sums in
 a geometric context. In addition to the explanations from the filters section, you will probably need
-<code class="docutils literal notranslate"><span class="pre">tendsto_pow_atTop_nhds_0_of_lt_1</span></code>, <code class="docutils literal notranslate"><span class="pre">Tendsto.mul</span></code> and <code class="docutils literal notranslate"><span class="pre">dist_le_range_sum_dist</span></code>.</p>
+<code class="docutils literal notranslate"><span class="pre">tendsto_pow_atTop_nhds_zero_of_lt_one</span></code>, <code class="docutils literal notranslate"><span class="pre">Tendsto.mul</span></code> and <code class="docutils literal notranslate"><span class="pre">dist_le_range_sum_dist</span></code>.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">cauchySeq_of_le_geometric_two&#39;</span><span class="w"> </span><span class="o">{</span><span class="n">u</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">X</span><span class="o">}</span>
 <span class="w">    </span><span class="o">(</span><span class="n">hu</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="o">))</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">CauchySeq</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">:=</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">Metric.cauchySeq_iff&#39;</span><span class="o">]</span>

C10_Differential_Calculus.html

@@ -285,10 +285,10 @@ <h3><span class="section-number">10.2.2. </span>Continuous linear maps<a class="
 <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">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span>
 
 <span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
-<span class="w">  </span><span class="n">f.le_op_norm</span><span class="w"> </span><span class="n">x</span>
+<span class="w">  </span><span class="n">f.le_opNorm</span><span class="w"> </span><span class="n">x</span>
 
 <span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hMp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hM</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="o">:=</span>
-<span class="w">  </span><span class="n">f.op_norm_le_bound</span><span class="w"> </span><span class="n">hMp</span><span class="w"> </span><span class="n">hM</span>
+<span class="w">  </span><span class="n">f.opNorm_le_bound</span><span class="w"> </span><span class="n">hMp</span><span class="w"> </span><span class="n">hM</span>
 </pre></div>
 </div>
 <p>There is also a notion of bundled continuous linear <em>isomorphism</em>.