This month in mathlib (Mar 2022)
March 2022 saw a record number of new contributions to mathlib: 682 PRs were merged, obliterating the old record of 565 merged PRs.

Algebra.
 After the definition of the Krull topology last month, PR #11973 and PR #12398 show the Krull topology is Hausdorff and totally disconnected
 Joachim Breitner contributed to group theory by establishing the Ping Pong Lemma in PR #12210, then PR #11778 completes the last in a chain of equivalences for finite nilpotent groups (direct product of Sylow subgroups), culiminating in PR #11835.
 PR #12866 A polynomial ring in arbitrarily many variables over a UFD is a UFD.
 PR #12300 Adds nonunital and nonassociative rings, thereby opening the door for applications elsewhere. For instance square matrices over a nonunital ring form a nonunital ring (PR #12913), nonunital normed rings (PR #12326), allow nonunital C∗rings (PR #12327), and define unitization of a nonunital algebra (PR #12601).
 PR #12041 Classifies 1d isocrystals in padic Hodge theory, and in so doing exhibits an application of the semilinear map refactor other than linear or conjugatelinear maps.
 PR #12485 Adds a nice counterexample to mathlib: a homogeneous ideal that is not prime but homogeneously prime. This can only occur in graded rings that are graded by a noncancellative monoid.
 PR #12634 The three subgroups lemma

Analysis
 This month saw the initial development of bornology in mathlib, defined in PR #12036 by means of the cobounded filter instead of as a collection of bounded sets. This was followed closely by locally bounded maps (PR #12046), the category
Born
of bornologies (PR #12045) and the natural bornology of von Neumann bounded sets in a locally convex space (PR #12449 and PR #12721).  Convexity itself also had significant developments, including: closed balanced sets are a basis of the topology (PR #12786), the topology of weak duals is locally convex (PR #12623), and an inner product space is strictly convex (PR #12790).
 Thanks to recent work in complex analysis, progress was made on the spectrum. Of particular interest are PR #12115 which shows that the spectrum in a complex Banach algebra is nonempty, and PR #12787 which proves the GelfandMazur theorem.
 PR #12329 Von Neumann algebras have landed in mathlib; Scott Morrison provided two definitions of a von Neumann algebra (concrete and abstract). There's still a long way to go before we can relate these definitions!
 Integration theory saw PR #12216 which defines local integrability, PR #12539 shows continuous functions with exponential decay are integrable, and PR #12408 establishes uniform integrability and the Vitali convergence theorem.
 In PR #12942 Sébastien Gouezel completed a vital refactor of the Bochner integral by removing the restriction of second countability on the codomain. This has the tremendous benefit of allowing the removal of assumptions of
measurable_space
,borel_space
andsecond_countable_topology
downstream.  Polish spaces were introduced in PR #12437 and then it was shown in PR #12448 that injective images of Borel sets in Polish spaces are Borel.
 Sébastien Gouezel had another striking addition in PR #12492: change of variable formula in integrals in higher dimension. This particular formulation is notable for its generality.
 This month saw the initial development of bornology in mathlib, defined in PR #12036 by means of the cobounded filter instead of as a collection of bounded sets. This was followed closely by locally bounded maps (PR #12046), the category

Category theory.
 Jujian Zhang dualized the existing material on projective resolutions, and as a consequence we now have right derived functors and some basic properties (PR #12545, PR #12841 and PR #12810)
 The coherence theorem (which we already had for monoidal categories) has been extended to bicategories, by Yuma Mizuno in PR #12155. We're now investigating writing tactics which make using coherence practical in proofs.

Model theory. Continuing last month's inauguration of model theory in mathlib, this month saw

Graph theory.

Probability theory. Foundational work in probability theory occurred in:

Number theory.

Linear algebra.

Algebraic geometry.

General. The community release of Lean was updated twice.

PR #12591 Updates to Lean 3.41.0c, which allows
sorry
to skip a tactic block, introduces the optionpp.numeral_types
to show numeral type ascriptions, and adds a search engine for finding relevant lemmas Lean PR #696. 
PR #12818 Updates to Lean 3.42.0c, which includes a fix for the "unknown declaration" error when rebuilding oleans involving
private
definitions, and adds anoncomputable!
modifier to completely inhibit VM compilation.

PR #12591 Updates to Lean 3.41.0c, which allows