typo

Co-authored-by: damiano <[email protected]>

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

@@ -31,7 +31,7 @@ There were 667 PRs merged in May 2024.
 * Analysis.
   * 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.
   * Sébastien Gouëzel completed the proof that the Fourier transform is well defined on the Schwartz space of a Euclidean space. [PR #12769](https://github.com/leanprover-community/mathlib4/pull/12769) shows how one can bound derivatives of the Fourier transform of a function (multiplied by a power function) in terms of derivatives of the initial function (multiplied by a power function) and [PR #11937](https://github.com/leanprover-community/mathlib4/pull/11937) proves a version of integration by parts for line/Fréchet derivatives. [PR #12144](https://github.com/leanprover-community/mathlib4/pull/12144) puts these results together to define the Fourier transform as a continuous linear equivalence on Schwartz space (taking advantage of the Fourier inversion formula to get the inverse direction from the forward direction). Note that the Schwartz space is a Fréchet space but not a normed space, so this builds on a lot of analysis on Fréchet spaces in terms of families of seminorms.
-  * Chris Birkbeck proved that Eisenstein series converge uniformly in [PR #10377](https://github.com/leanprover-community/mathlib4/pull/10377) and that they are holomorphic in [PR #11013](https://github.com/leanprover-community/mathlib4/pull/11013). This will soon to used to show that they are modular forms.
+  * Chris Birkbeck proved that Eisenstein series converge uniformly in [PR #10377](https://github.com/leanprover-community/mathlib4/pull/10377) and that they are holomorphic in [PR #11013](https://github.com/leanprover-community/mathlib4/pull/11013). This will soon be used to show that they are modular forms.
   * Xavier Généreux proved the Hadamard three-lines theorem in the special case of the unit vertical strip in [PR #7919](https://github.com/leanprover-community/mathlib4/pull/7919). This will be used to interpolate norms.
   * In [PR #12669], Mitchell Lee proved that the completion of a nonarchimedean group is again nonarchimedean.
   * In [PR #12432](https://github.com/leanprover-community/mathlib4/pull/12432), it is shown that non-trivial non-archimedean norms correspond to rank 1 valuations.