This month in mathlib (Sep 2022)
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

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

Combinatorics

Model theory
 PR #16548 defines the space of complete types over a firstorder theory.

Number theory

PR #15000 proves the DedekindKummer theorem for a ring extension
R[α]/R
, showing the primes over a prime idealp
are determined by the factorization of the minimal polynomial ofα
in the quotient ringR/p
. We are currently working on extending this theorem to the nonmonogenic case.  PR #15646 defines Sintegers and Sunits.

PR #15000 proves the DedekindKummer theorem for a ring extension