# 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.

• PR #16830 improves Vitali families and Lebesgue density theorem.
• PR #16762 adds a version of Lebesgue's density theorem.
• PR #16906 proves Lebesgue differentiation theorem.
• PR #16836 relates integrals over add_circle with integrals upstairs in .
• 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 Artin-Rees lemma and Krull's intersection theorems.
• PR #16317 adds the multinomial theorem.
• PR #17295 proves the Jordan-Hö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 non-unital 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 Hahn-Banach 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.

• PR #15405 introduces the Selmer group of a Dedekind domain.
• PR #17677 defines slash-invariant forms, a step towards the definition of modular forms.
• PR #17203 defines the absolute ideal norm.
• Representation theory.

• PR #17005 is about exactness properties of resolutions.
• PR #16043 proves the orthogonality of characters.
• PR #13794 proves Schur's lemma.
• PR #17443 adds the construction of a projective resolution of a representation.
• 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.

• PR #11468 shows that the clifford algebra is isomorphic as a module to the exterior algebra.
• PR #16150 proves that the inverse of a block triangular matrix is block triangular.
• Category theory.

• PR #16313 introduces the qify tactic, to move from $\mathbb{Z}$ to $\mathbb{Q}$.