Skip to main content

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.