This month in mathlib (Sep 2022)

In September 2022 there were 361 PRs merged into mathlib. We list some of the highlights below.

• Analysis

• Probability theory

• PR #16532 proves uniqueness of Doob's decomposition.
• PR #16358 proves Lévy's generalized Borel-Cantelli.
• Algebraic topology

• PR #16403 proves the category of sheaves on a site with values is an abelian category is abelian. It also proves that sheafification is an additive functor.
• Geometry

• PR #16243 has many lemmas about signs of angles between linear combinations of vectors.
• PR #14703 and PR #15009 are working towards hyperbolic geometry in dimension 2 with a eye towards modular forms.
• Combinatorics

• PR #16120 continues developping the theory of Young diagrams.
• PR #15440 proves the Plünnecke-Ruzsa inequality.
• Model theory

• PR #16548 defines the space of complete types over a first-order theory.
• Number theory

• PR #15000 proves the Dedekind-Kummer theorem for a ring extension R[α]/R, showing the primes over a prime ideal p are determined by the factorization of the minimal polynomial of α in the quotient ring R/p. We are currently working on extending this theorem to the non-monogenic case.
• PR #15646 defines S-integers and S-units.