This month in mathlib (Oct and Nov 2022)
In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below.

Measure theory.

Algebra.
 PR #14672 defines mixed/equal characteristic zero.
 PR #17018, PR #16849 and PR #17011 show the Kähler differential module is functorial and that $S/R$ is formally unramified if and only if $\Omega^1_{S/R} = 0$. They also give the standard presentation of the Kähler differential module.
 PR #16000 proves ArtinRees lemma and Krull's intersection theorems.
 PR #16317 adds the multinomial theorem.
 PR #17295 proves the JordanHölder theorem for modules.
 PR #17311 proves that a group with finitely many commutators has finite commutator subgroup.
 PR #17243 proves the Third Isomorphism theorem for rings.
 PR #13749 introduces nonunital subsemirings.

Analysis
 PR #16723 shows that two analytic functions that coincide locally coincide globally.
 PR #16683 and PR #16680 introduce functions of bounded variation and prove that they are almost everywhere differentiable. As a corollary, PR #16549 shows that a monotone function is differentiable almost everywhere.
 PR #17119 defines and gives basic properties of the complex unit disc.
 PR #16780 proves the open mapping theorem for holomorphic functions.
 PR #16487 constructs the volume form.
 PR #16796 generalizes the HahnBanach separation theorem to (locally convex) topological vector spaces.
 PR #16835 proves functoriality of the character space.
 PR #16638 introduces the Dirac delta distribution.
 PR #17110 proves smoothness of series of functions.
 PR #16201 and PR #17598 define the additive circle and develop Fourier analysis on it.
 PR #17543 computes $\Gamma(1/2)$.
 PR #16053 introduces the strong operator topology.

Number theory.

Representation theory.

Topology.
 PR #16677 constructs the Galois correspondence between closed ideals in $C(X, 𝕜)$ and open sets in $X$.
 PR #16719 shows that maximal ideals of $C(X, 𝕜)$ correspond to (complements of) singletons.
 PR #16087 defines covering spaces.
 PR #16797 proves that the stalk functor preserves monomorphism.
 PR #17015 proves that Noetherian spaces have finite irreducible components.

Probability theory.

Algebraic and differential geometry.

Linear algebra.

Category theory.
 PR #16969 adds basic results about localization of categories.

Combinatorics
 PR #16195 adds the definition and some basic results about semistandard Young tableaux.
 PR #17445 adds an equivalence between Young diagrams and weakly decreasing lists of positive natural numbers.
 PR #17306 and PR #17213 define bridge edges, acyclic graphs, and trees for simple graphs, and provide some characterizations.

Tactics
During these two months, we got two new versions of Lean. We also started to systematically port mathlib to Lean4, see the wiki.