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

• Analysis

  • PR #14874 and PR #14875 brought us Stirling's formula.
  • PR #15087 proves Taylor's formula with various kinds of remainders, hence filling an important gap in our undergrad math coverage.
  • PR #15908 proves the principle of isolated zeros in complex analysis.
  • PR #15850 defines of the Schwartz space, aiming for tempered distributions.

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