Update mim-2024-05.md

leanprover-community · Jul 1, 2024 · 4543251 · 4543251
1 parent 4f7d251
commit 4543251
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/posts/month-in-mathlib/2024/mim-2024-05.md b/posts/month-in-mathlib/2024/mim-2024-05.md
@@ -41,7 +41,7 @@ There were 667 PRs merged in May 2024.
       The definition was in [PR #10091](https://github.com/leanprover-community/mathlib4/pull/10091), and the fact that oplax monoidal functors (newly defined in [PR #12856](https://github.com/leanprover-community/mathlib4/pull/12856))
       take comonoids to comonoids in
       [PR #12858](https://github.com/leanprover-community/mathlib4/pull/12858). In a braided category, the comonoid objects themselves have a monoidal category structure,
-      developed in [PR #10098](https://github.com/leanprover-community/mathlib4/pull/10098). Finally, in a cartesion monoidal category, comonoids are not interesting:
+      developed in [PR #10098](https://github.com/leanprover-community/mathlib4/pull/10098). Finally, in a cartesian monoidal category, comonoids are not interesting:
       every object is a comonoid object in a unique way, using the diagonal map as the comultiplication. This is proved in [PR #10103](https://github.com/leanprover-community/mathlib4/pull/10103).
 
 * Combinatorics.
@@ -86,4 +86,4 @@ There were 667 PRs merged in May 2024.
         * In a similar fashion, some simp lemmas accidentally had a lambda on their LHS, meaning that their key in simp's discrimination tree was maximally general and that simp would try rewriting with them in every location. Some such lemmas were unsimped in [PR #13164](https://github.com/leanprover-community/mathlib4/pull/13164).
     * A sustained effort has started to reduce spurious dependencies between files. There are two lines of work:
         * Reducing the long pole: Assuming Mathlib is built on an infinitely parallelizing machine, there is some sequence of files, each importing the previous, that takes the longest to build. We call this sequence the "long pole". As it is a cap on performance, it is natural to try shortening it. After [PR #12777](https://github.com/leanprover-community/mathlib4/pull/12777), [PR #12401](https://github.com/leanprover-community/mathlib4/pull/12401), the long pole has left the `RingTheory` folder entirely.
-        * Reducing imports to basic files: The theory of basic algebra, order theory and data structures feed into each other at various points. For example, we need to know some order properties of addition and multiplication on `Nat` and `Int` to talk about powers in a group, and we need finite sets to define finite sums and finite suprema/infima. It is overwhelmingly easy to create an almost-circular import graph ricocheting between those three areas. The `Nat`- and `Int`-specific lemmas in Core and Batteries are an opportunity to cut the knot: These lemmas do not depend on Mathlib's algebraic order hierarchy, hence can be used in basic algebra and data structures without over-importing. The following PRs are steps towards that: [PR #11986](https://github.com/leanprover-community/mathlib4/pull/11986), [PR #12710](https://github.com/leanprover-community/mathlib4/pull/12710), [PR #12828](https://github.com/leanprover-community/mathlib4/pull/12828), [PR #12736](https://github.com/leanprover-community/mathlib4/pull/12736), [PR #12825](https://github.com/leanprover-community/mathlib4/pull/12825), [PR #12817](https://github.com/leanprover-community/mathlib4/pull/12817), [PR #12823](https://github.com/leanprover-community/mathlib4/pull/12823), [PR #12872](https://github.com/leanprover-community/mathlib4/pull/12872), [PR #12829](https://github.com/leanprover-community/mathlib4/pull/12829), [PR #12862](https://github.com/leanprover-community/mathlib4/pull/12862), [PR #12835](https://github.com/leanprover-community/mathlib4/pull/12835), [PR #12821](https://github.com/leanprover-community/mathlib4/pull/12821), [PR #12818](https://github.com/leanprover-community/mathlib4/pull/12818), [PR #12836](https://github.com/leanprover-community/mathlib4/pull/12836), [PR #12832](https://github.com/leanprover-community/mathlib4/pull/12832), [PR #12882](https://github.com/leanprover-community/mathlib4/pull/12882), [PR #12975](https://github.com/leanprover-community/mathlib4/pull/12975), [PR #11855](https://github.com/leanprover-community/mathlib4/pull/11855), [PR #13029](https://github.com/leanprover-community/mathlib4/pull/13029), [PR #12985](https://github.com/leanprover-community/mathlib4/pull/12985), [PR #13008](https://github.com/leanprover-community/mathlib4/pull/13008), [PR #13033](https://github.com/leanprover-community/mathlib4/pull/13033), [PR #12845](https://github.com/leanprover-community/mathlib4/pull/12845), [PR #12974](https://github.com/leanprover-community/mathlib4/pull/12974), [PR #11863](https://github.com/leanprover-community/mathlib4/pull/11863), [PR #12959](https://github.com/leanprover-community/mathlib4/pull/12959), [PR #13030](https://github.com/leanprover-community/mathlib4/pull/13030), [PR #13031](https://github.com/leanprover-community/mathlib4/pull/13031), [PR #13005](https://github.com/leanprover-community/mathlib4/pull/13005), [PR #13140](https://github.com/leanprover-community/mathlib4/pull/13140), [PR #13139](https://github.com/leanprover-community/mathlib4/pull/13139), [PR #12990](https://github.com/leanprover-community/mathlib4/pull/12990), [PR #13184](https://github.com/leanprover-community/mathlib4/pull/13184), [PR #13197](https://github.com/leanprover-community/mathlib4/pull/13197), [PR #13138](https://github.com/leanprover-community/mathlib4/pull/13138), [PR #12957](https://github.com/leanprover-community/mathlib4/pull/12957), [PR #13222](https://github.com/leanprover-community/mathlib4/pull/13222), [PR #13224](https://github.com/leanprover-community/mathlib4/pull/13224), [PR #13242](https://github.com/leanprover-community/mathlib4/pull/13242), [PR #13288](https://github.com/leanprover-community/mathlib4/pull/13288), [PR #13003](https://github.com/leanprover-community/mathlib4/pull/13003), [PR #13205](https://github.com/leanprover-community/mathlib4/pull/13205), [PR #13289](https://github.com/leanprover-community/mathlib4/pull/13289), [PR #13244](https://github.com/leanprover-community/mathlib4/pull/13244), [PR #13305](https://github.com/leanprover-community/mathlib4/pull/13305), [PR #13274](https://github.com/leanprover-community/mathlib4/pull/13274), [PR #13253](https://github.com/leanprover-community/mathlib4/pull/13253), [PR #13268](https://github.com/leanprover-community/mathlib4/pull/13268), [PR #13147](https://github.com/leanprover-community/mathlib4/pull/13147), [PR #13243](https://github.com/leanprover-community/mathlib4/pull/13243).
+        * Reducing imports to basic files: The theory of basic algebra, order theory and data structures feed into each other at various points. For example, we need to know some order properties of addition and multiplication on `Nat` and `Int` to talk about powers in a group, and we need finite sets to define finite sums and finite suprema/infima. It is overwhelmingly easy to create an almost-circular import graph ricocheting between those three areas. The `Nat`- and `Int`-specific lemmas in Core and Batteries are an opportunity to cut the knot: These lemmas do not depend on Mathlib's algebraic order hierarchy, hence can be used in basic algebra and data structures without over-importing. The following PRs are steps towards that: [PR #11986](https://github.com/leanprover-community/mathlib4/pull/11986), [PR #12710](https://github.com/leanprover-community/mathlib4/pull/12710), [PR #12828](https://github.com/leanprover-community/mathlib4/pull/12828), [PR #12736](https://github.com/leanprover-community/mathlib4/pull/12736), [PR #12825](https://github.com/leanprover-community/mathlib4/pull/12825), [PR #12817](https://github.com/leanprover-community/mathlib4/pull/12817), [PR #12823](https://github.com/leanprover-community/mathlib4/pull/12823), [PR #12872](https://github.com/leanprover-community/mathlib4/pull/12872), [PR #12829](https://github.com/leanprover-community/mathlib4/pull/12829), [PR #12862](https://github.com/leanprover-community/mathlib4/pull/12862), [PR #12835](https://github.com/leanprover-community/mathlib4/pull/12835), [PR #12821](https://github.com/leanprover-community/mathlib4/pull/12821), [PR #12818](https://github.com/leanprover-community/mathlib4/pull/12818), [PR #12836](https://github.com/leanprover-community/mathlib4/pull/12836), [PR #12832](https://github.com/leanprover-community/mathlib4/pull/12832), [PR #12882](https://github.com/leanprover-community/mathlib4/pull/12882), [PR #12975](https://github.com/leanprover-community/mathlib4/pull/12975), [PR #11855](https://github.com/leanprover-community/mathlib4/pull/11855), [PR #13029](https://github.com/leanprover-community/mathlib4/pull/13029), [PR #12985](https://github.com/leanprover-community/mathlib4/pull/12985), [PR #13008](https://github.com/leanprover-community/mathlib4/pull/13008), [PR #13033](https://github.com/leanprover-community/mathlib4/pull/13033), [PR #12845](https://github.com/leanprover-community/mathlib4/pull/12845), [PR #12974](https://github.com/leanprover-community/mathlib4/pull/12974), [PR #11863](https://github.com/leanprover-community/mathlib4/pull/11863), [PR #12959](https://github.com/leanprover-community/mathlib4/pull/12959), [PR #13030](https://github.com/leanprover-community/mathlib4/pull/13030), [PR #13031](https://github.com/leanprover-community/mathlib4/pull/13031), [PR #13005](https://github.com/leanprover-community/mathlib4/pull/13005), [PR #13140](https://github.com/leanprover-community/mathlib4/pull/13140), [PR #13139](https://github.com/leanprover-community/mathlib4/pull/13139), [PR #12990](https://github.com/leanprover-community/mathlib4/pull/12990), [PR #13184](https://github.com/leanprover-community/mathlib4/pull/13184), [PR #13197](https://github.com/leanprover-community/mathlib4/pull/13197), [PR #13138](https://github.com/leanprover-community/mathlib4/pull/13138), [PR #12957](https://github.com/leanprover-community/mathlib4/pull/12957), [PR #13222](https://github.com/leanprover-community/mathlib4/pull/13222), [PR #13224](https://github.com/leanprover-community/mathlib4/pull/13224), [PR #13242](https://github.com/leanprover-community/mathlib4/pull/13242), [PR #13288](https://github.com/leanprover-community/mathlib4/pull/13288), [PR #13003](https://github.com/leanprover-community/mathlib4/pull/13003), [PR #13205](https://github.com/leanprover-community/mathlib4/pull/13205), [PR #13289](https://github.com/leanprover-community/mathlib4/pull/13289), [PR #13244](https://github.com/leanprover-community/mathlib4/pull/13244), [PR #13305](https://github.com/leanprover-community/mathlib4/pull/13305), [PR #13274](https://github.com/leanprover-community/mathlib4/pull/13274), [PR #13253](https://github.com/leanprover-community/mathlib4/pull/13253), [PR #13268](https://github.com/leanprover-community/mathlib4/pull/13268), [PR #13147](https://github.com/leanprover-community/mathlib4/pull/13147), [PR #13243](https://github.com/leanprover-community/mathlib4/pull/13243).