David's and Mitchell's paragraphs

Co-authored-by: Mitchell Lee <[email protected]>
Co-authored-by: David Loeffler <[email protected]>

posts/month-in-mathlib-may-2024.md

@@ -23,10 +23,8 @@ There were 667 PRs merged in May 2024.
   * Amelia Livingston added some boilerplate defining coalgebra isomorphisms in [PR #11970](https://github.com/leanprover-community/mathlib4/pull/11970), the category of coalgebras in [PR #11972](https://github.com/leanprover-community/mathlib4/pull/11972), and homomorphisms and isomorphisms of bialgebras in [PR #11962](https://github.com/leanprover-community/mathlib4/pull/11962) and [PR #11971](https://github.com/leanprover-community/mathlib4/pull/11971). This API will be used to define the monoidal category structure on co/bi/Hopf algebras. It will also be linked to Kim Morrison's work on co/bi/Hopf monoids, as well as the material about group objects formalised at [Formalisation of Mathematics: Workshop for Women and Mathematicians of Minority Gender](https://www.icms.org.uk/Formalisation) with Rebecca Bellovin and Sophie Morel.
   * Joël Riou
     * [PR #12713](https://github.com/leanprover-community/mathlib4/pull/12713) :: feat(Algebra/Category/ModuleCat): the category of presheaves of modules has colimits
-  * Mitchell Lee
-    * [PR #11465](https://github.com/leanprover-community/mathlib4/pull/11465) :: feat: length, reduced words in Coxeter groups
-    * [PR #11466](https://github.com/leanprover-community/mathlib4/pull/11466) :: feat: reflections, inversion sequences in Coxeter groups
-    * [PR #12647](https://github.com/leanprover-community/mathlib4/pull/12647) :: feat: the equational criterion for vanishing
+* Mitchell Lee laid the groundwork for future material on Coxeter groups. [PR #11465] defines the length function on a Coxeter group and proves its basic properties. [PR #11466] defines reflections and inversions in a Coxeter group and proves that the inversion sequence of a reduced word consists of distinct reflections.
+* In [PR #12647], Mitchell Lee formalized a proof of the equational criterion for vanishing, a necessary and sufficient criterion for a sum of pure tensors in the tensor product of two modules to vanish.
   * Oliver Nash
     * [PR #13208](https://github.com/leanprover-community/mathlib4/pull/13208) :: feat: equality of coroots implies equality of roots for Lie algebras
     * [PR #13298](https://github.com/leanprover-community/mathlib4/pull/13298) :: feat(Algebra/Lie/Weights): `n` such that `n • α + β` is a weight is consecutive.
@@ -69,8 +67,7 @@ There were 667 PRs merged in May 2024.
   * Xavier Généreux
     * [PR #7919](https://github.com/leanprover-community/mathlib4/pull/7919) :: feat: Hadamard three-lines theorem
   * Jireh Loreaux and Anatole Dedecker completed the development of the non-unital continuous functional calculus. Although the generic API has been in place for a few months, the relevant instances for C⋆-algebras were missing. Work progressed in a piecemeal fashion, but [PR #13326](https://github.com/leanprover-community/mathlib4/pull/13326) provides a version of the Stone-Weiertrass theorem for continuous functions vanishing at zero, namely that the non-unital star subalgebra generated by the identity function is dense. This is essential for [PR #13363](https://github.com/leanprover-community/mathlib4/pull/13363) which provides uniqueness instances for the non-unital continuous functional calculus. Then [PR #13327](https://github.com/leanprover-community/mathlib4/pull/13327) and [PR #13365](https://github.com/leanprover-community/mathlib4/pull/13365) provide instances of the non-unital continuous functional calculus for non-unital C⋆-algebras and generic restriction lemmas for scalar subrings. These are obtained by first considering the unitization of the algebra, obtaining a unital functional calculus there, and then realizing a non-unital functional calculus by appropriately restricting the unital one to functions vanishing at zero. Finally, [PR #13541](https://github.com/leanprover-community/mathlib4/pull/13541) obtains a non-unital continuous functional calculus from a unital one, which will be necessary to get a non-unital instance on matrices, for example.
-  * Mitchell Lee
-    * [PR #12669](https://github.com/leanprover-community/mathlib4/pull/12669) :: feat: completion of a nonarchimedean additive group
+  * In [PR #12669], Mitchell Lee proved that the completion of a nonarchimedean group is again nonarchimedean.
   * Jeremy Toh
     * [PR #8806](https://github.com/leanprover-community/mathlib4/pull/8806) :: feat(Analysis/PSeries): add Schlömilch's generalization of the Cauchy condensation test
   * María Inés de Frutos-Fernández
@@ -144,11 +141,7 @@ There were 667 PRs merged in May 2024.
 
 * Number Theory.
   * David Loeffler
-    * [PR #12265](https://github.com/leanprover-community/mathlib4/pull/12265) :: feat(NumberTheory/LSeries): Even Hurwitz zeta functions (II)
-    * [PR #12779](https://github.com/leanprover-community/mathlib4/pull/12779) :: feat(NumberTheory/LSeries): Odd Hurwitz zeta functions
-    * [PR #12897](https://github.com/leanprover-community/mathlib4/pull/12897) :: feat (NumberTheory/LSeries): Hurwitz zeta
-    * [PR #13347](https://github.com/leanprover-community/mathlib4/pull/13347) :: feat(NumberTheory/LSeries): special values of Hurwitz zeta
-    * [PR #13273](https://github.com/leanprover-community/mathlib4/pull/13273) :: feat(NumberTheory/LSeries): Riemann zeta as special case of Hurwitz
+    * [PR #12897](https://github.com/leanprover-community/mathlib4/pull/12897) defines the **Hurwitz zeta function**, and proves its key properties (analytic continuation + functional equation). This is a generalisation of the Riemann zeta function, and is an important step towards Dirichlet L-functions in the near future. (Subsidiary PR's include [PR #12779](https://github.com/leanprover-community/mathlib4/pull/12779), [PR #12265](https://github.com/leanprover-community/mathlib4/pull/12265), [PR #13347](https://github.com/leanprover-community/mathlib4/pull/13347), [PR #13273](https://github.com/leanprover-community/mathlib4/pull/13273).)
     * [PR #12923](https://github.com/leanprover-community/mathlib4/pull/12923) :: feat (NumberTheory/Harmonic): compute Gamma'(1/2)
   * Riccardo Brasca
     * [PR #12977](https://github.com/leanprover-community/mathlib4/pull/12977) :: feat(NumberTheory.FLT.Three): basic properties of a solution to flt3