This month in mathlib (Aug 2021)
This post summarizes some of the activity that happened in mathlib in August.
Highlighted PRs

PR #8652: chore(*): update lean to 3.32.1
The community fork of Lean made two new releases3.32.0
and3.32.1
. This is part of the preparations for porting mathlib to Lean 4. 
PR #8281: continuous and smooth partition of unity
See the companion blogpost for details. 
RadonNikodym and Lebesgue decomposition. The four PRs PR #8645 PR #8687 PR #8763 PR #8875 together contribute the Lebesgue decomposition for sigmafinite measures and the RadonNikodym theorem.

PR #7978: strong version of FTC2
This weakens considerably the assumptions of part of the fundamental theorem of calculus: $\int _{a}^{b}f'(x)\,dx=f(b)f(a)$, replacing continuity of $f'$ by the much more natural assumption of integrability. 
PR #4885: general adjoint functor theorem: If $G : D ⇒ C$ preserves limits and $D$ has limits, and satisfies the solution set condition, then it has a left adjoint.

PR #8692: finite fields exist
Most of this PR had been lying around for ages, but it was finally put together in mathlib. It shows the existence and uniqueness up to isomorphism of a finite field with cardinal $p^n$ for any prime number $p$ and positive integer $n$. 
Among several PRs from the Dedekind project, the two most noteworthy are

PR #8377: new file
This PR defines the complex upper half plane, together with the $\mathrm{SL}_2$action.
Upcoming PRs will characterize the fundamental domain of the $\mathrm{SL}_2(\mathbb{Z})$action.
Other mathematical contributions
The following PRs are ordered by the date that they were merged into mathlib.
 PR #8424: prove that complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential
 PR #8560: Add the Kronecker product
 PR #8388: signed version of the Hahn decomposition theorem
 PR #8588: Smith normal form for submodules over a PID This PR is a step towards the classification of finite type modules over a PID.
 PR #8266: Stieltjes measures associated to monotone functions
 PR #8598: add definition and first lemmas about weakstar topology
 PR #8639: prove Haar measure = Lebesgue measure on $ℝ$
 PR #8558: add working definition of elliptic curve
 PR #8538: add nilpotent groups
 PR #8343: generalize inequalities and invariance of dimension to arbitrary rings
 PR #8791: volume of a (closed) $L^∞$ball
 PR #8576: define exponential in a Banach algebra and prove basic results