deploy site from 99bbdb1

Author: leanprover-community-bot

docs/authors/adam-topaz.xml

@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Adam Topaz)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/adam-topaz.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 12:40:45 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Definitions in the liquid tensor experiment</title><link>https://leanprover-community.github.io/blog/posts/lte-examples/</link><dc:creator>Adam Topaz</dc:creator><description>&lt;div&gt;&lt;p&gt;A few weeks ago, we announced the &lt;a href="https://leanprover-community.github.io/blog/posts/lte-final/"&gt;completion of the liquid tensor experiment&lt;/a&gt; (&lt;strong&gt;LTE&lt;/strong&gt; for short).
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Adam Topaz)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/adam-topaz.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 13:09:23 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Definitions in the liquid tensor experiment</title><link>https://leanprover-community.github.io/blog/posts/lte-examples/</link><dc:creator>Adam Topaz</dc:creator><description>&lt;div&gt;&lt;p&gt;A few weeks ago, we announced the &lt;a href="https://leanprover-community.github.io/blog/posts/lte-final/"&gt;completion of the liquid tensor experiment&lt;/a&gt; (&lt;strong&gt;LTE&lt;/strong&gt; for short).
 What this means is that we stated and (completely) proved the following result in Lean:&lt;/p&gt;
 &lt;pre class="code literal-block"&gt;&lt;span class="kd"&gt;variables&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="n"&gt;p'&lt;/span&gt; &lt;span class="n"&gt;p&lt;/span&gt; &lt;span class="o"&gt;:&lt;/span&gt; &lt;span class="n"&gt;ℝ&lt;/span&gt;&lt;span class="bp"&gt;≥&lt;/span&gt;&lt;span class="mi"&gt;0&lt;/span&gt;&lt;span class="o"&gt;)&lt;/span&gt; &lt;span class="o"&gt;[&lt;/span&gt;&lt;span class="n"&gt;fact&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="mi"&gt;0&lt;/span&gt; &lt;span class="bp"&gt;&amp;lt;&lt;/span&gt; &lt;span class="n"&gt;p'&lt;/span&gt;&lt;span class="o"&gt;)]&lt;/span&gt; &lt;span class="o"&gt;[&lt;/span&gt;&lt;span class="n"&gt;fact&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="n"&gt;p'&lt;/span&gt; &lt;span class="bp"&gt;&amp;lt;&lt;/span&gt; &lt;span class="n"&gt;p&lt;/span&gt;&lt;span class="o"&gt;)]&lt;/span&gt; &lt;span class="o"&gt;[&lt;/span&gt;&lt;span class="n"&gt;fact&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="n"&gt;p&lt;/span&gt; &lt;span class="bp"&gt;≤&lt;/span&gt; &lt;span class="mi"&gt;1&lt;/span&gt;&lt;span class="o"&gt;)]&lt;/span&gt;
 

docs/authors/anne-baanen.xml

@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Anne Baanen)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/anne-baanen.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 12:40:45 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Dedekind domains and class number in Lean</title><link>https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/</link><dc:creator>Anne Baanen</dc:creator><description>&lt;div&gt;&lt;p&gt;Pull request &lt;a href="https://github.com/leanprover-community/mathlib/pull/9071"&gt;#9701&lt;/a&gt; marks the completion of a string of additions to mathlib centered around formalizing Dedekind domains and class groups of global fields (those words will be explained below). Previous PRs had shown that nonzero ideals of a Dedekind domain factor uniquely into prime ideals, and had defined class groups in some generality. The main result in this PR is the finiteness of the class group of a global field (and in particular of the ring of integers of a number field).
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Anne Baanen)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/anne-baanen.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 13:09:22 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Dedekind domains and class number in Lean</title><link>https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/</link><dc:creator>Anne Baanen</dc:creator><description>&lt;div&gt;&lt;p&gt;Pull request &lt;a href="https://github.com/leanprover-community/mathlib/pull/9071"&gt;#9701&lt;/a&gt; marks the completion of a string of additions to mathlib centered around formalizing Dedekind domains and class groups of global fields (those words will be explained below). Previous PRs had shown that nonzero ideals of a Dedekind domain factor uniquely into prime ideals, and had defined class groups in some generality. The main result in this PR is the finiteness of the class group of a global field (and in particular of the ring of integers of a number field).
 Formalizing these subjects has been one of my long-term goals for mathlib,
 and as far as we are aware, Lean is the first system in which this level of algebraic number theory is available.
 These formalizations have been joint work:

docs/authors/chris-birkbeck.xml

@@ -1,3 +1,3 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Chris Birkbeck)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/chris-birkbeck.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 12:40:45 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Modular forms</title><link>https://leanprover-community.github.io/blog/posts/modular-forms/</link><dc:creator>Chris Birkbeck</dc:creator><description>&lt;div&gt;&lt;p&gt;In &lt;a href="https://github.com/leanprover-community/mathlib/pull/13250"&gt;PR# 13250&lt;/a&gt; we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.&lt;/p&gt;
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Chris Birkbeck)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/chris-birkbeck.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 13:09:23 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Modular forms</title><link>https://leanprover-community.github.io/blog/posts/modular-forms/</link><dc:creator>Chris Birkbeck</dc:creator><description>&lt;div&gt;&lt;p&gt;In &lt;a href="https://github.com/leanprover-community/mathlib/pull/13250"&gt;PR# 13250&lt;/a&gt; we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.&lt;/p&gt;
 &lt;p&gt;&lt;a href="https://leanprover-community.github.io/blog/posts/modular-forms/"&gt;Read more…&lt;/a&gt; (7 min remaining to read)&lt;/p&gt;&lt;/div&gt;</description><guid>https://leanprover-community.github.io/blog/posts/modular-forms/</guid><pubDate>Wed, 21 Dec 2022 11:41:21 GMT</pubDate></item></channel></rss>

docs/authors/david-chanin.xml

@@ -1,4 +1,4 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by David Chanin)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/david-chanin.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 12:40:45 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Introducing Mathlib Changelog</title><link>https://leanprover-community.github.io/blog/posts/mathlib-changelog/</link><dc:creator>David Chanin</dc:creator><description>&lt;div&gt;&lt;p&gt;&lt;img alt="mathlib-changelog sample page" src="https://leanprover-community.github.io/blog/images/changelog_lemma.png"&gt;&lt;/p&gt;
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by David Chanin)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/david-chanin.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 13:09:22 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Introducing Mathlib Changelog</title><link>https://leanprover-community.github.io/blog/posts/mathlib-changelog/</link><dc:creator>David Chanin</dc:creator><description>&lt;div&gt;&lt;p&gt;&lt;img alt="mathlib-changelog sample page" src="https://leanprover-community.github.io/blog/images/changelog_lemma.png"&gt;&lt;/p&gt;
 &lt;p&gt;Tldr; check out &lt;a href="https://mathlib-changelog.org"&gt;mathlib-changelog.org&lt;/a&gt; to explore the historical changes to mathlib, and find out what happened to that lemma you were using.&lt;/p&gt;
 &lt;p&gt;&lt;a href="https://leanprover-community.github.io/blog/posts/mathlib-changelog/"&gt;Read more…&lt;/a&gt; (3 min remaining to read)&lt;/p&gt;&lt;/div&gt;</description><guid>https://leanprover-community.github.io/blog/posts/mathlib-changelog/</guid><pubDate>Thu, 28 Jul 2022 07:35:23 GMT</pubDate></item></channel></rss>

docs/authors/frederic-dupuis.xml

@@ -1,3 +1,3 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Frédéric Dupuis)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/frederic-dupuis.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 12:40:45 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Semilinear maps</title><link>https://leanprover-community.github.io/blog/posts/semilinear-maps/</link><dc:creator>Frédéric Dupuis</dc:creator><description>&lt;div&gt;&lt;p&gt;Since linear maps appear everywhere in mathematics, it comes as no surprise that they have been part of mathlib for quite some time. However, as we were working on adding the basics of functional analysis to mathlib, a drawback quickly became apparent: conjugate-linear maps could not directly be expressed as linear maps. This meant that some constructions could not be formulated in their most natural way: for example, the map that takes an operator to its adjoint on a complex Hilbert space is a conjugate linear map, and so is the Riesz representation that maps a vector to its dual. This was also preventing us from developing the orthogonal group, the unitary group, etc, properly.&lt;/p&gt;
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Frédéric Dupuis)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/frederic-dupuis.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 13:09:22 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Semilinear maps</title><link>https://leanprover-community.github.io/blog/posts/semilinear-maps/</link><dc:creator>Frédéric Dupuis</dc:creator><description>&lt;div&gt;&lt;p&gt;Since linear maps appear everywhere in mathematics, it comes as no surprise that they have been part of mathlib for quite some time. However, as we were working on adding the basics of functional analysis to mathlib, a drawback quickly became apparent: conjugate-linear maps could not directly be expressed as linear maps. This meant that some constructions could not be formulated in their most natural way: for example, the map that takes an operator to its adjoint on a complex Hilbert space is a conjugate linear map, and so is the Riesz representation that maps a vector to its dual. This was also preventing us from developing the orthogonal group, the unitary group, etc, properly.&lt;/p&gt;
 &lt;p&gt;&lt;a href="https://leanprover-community.github.io/blog/posts/semilinear-maps/"&gt;Read more…&lt;/a&gt; (4 min remaining to read)&lt;/p&gt;&lt;/div&gt;</description><guid>https://leanprover-community.github.io/blog/posts/semilinear-maps/</guid><pubDate>Sat, 11 Dec 2021 11:00:00 GMT</pubDate></item></channel></rss>

docs/authors/heather-macbeth.xml

@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Heather Macbeth)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/heather-macbeth.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 12:40:45 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Classification of one-dimensional isocrystals</title><link>https://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/</link><dc:creator>Robert Y. Lewis, Heather Macbeth</dc:creator><description>&lt;div&gt;&lt;p&gt;Last year, there was a &lt;a href="https://leanprover-community.github.io/blog/posts/semilinear-maps"&gt;big mathlib refactor&lt;/a&gt; to replace linear maps throughout the library with  &lt;em&gt;semilinear maps&lt;/em&gt;,
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Heather Macbeth)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/heather-macbeth.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 01 Jul 2024 13:09:22 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Classification of one-dimensional isocrystals</title><link>https://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/</link><dc:creator>Robert Y. Lewis, Heather Macbeth</dc:creator><description>&lt;div&gt;&lt;p&gt;Last year, there was a &lt;a href="https://leanprover-community.github.io/blog/posts/semilinear-maps"&gt;big mathlib refactor&lt;/a&gt; to replace linear maps throughout the library with  &lt;em&gt;semilinear maps&lt;/em&gt;,
 a more abstract concept which, importantly, unifies linear and conjugate-linear maps.&lt;/p&gt;
 &lt;p&gt;But this is not the full extent of the generalization!  Our number theorist friends here in mathlib told us that we should
 make sure we chose this full generality of &lt;em&gt;semilinear&lt;/em&gt; maps, maps $f:M \to N$ such that $f(ax)=\sigma(a)f(x)$ for some ring homomorphism $\sigma$ between the scalar rings of the modules $M$ and $N$.  So we and our coauthor Frédéric Dupuis implemented this full generality, and then asked them for an example to illustrate their need for this more abstract definition. This blog post tells the story of our little adventure in number theory.&lt;/p&gt;