This month in mathlib (Feb 2022)
February 2022 saw 501 commits to mathlib. In this post we highlight some of these contributions.
Model theory. This month saw a serious push to get model theory off the ground, partly leveraging work from the Flypitch project. The series of PRs PR #11089, PR #11906, PR #11789, PR #11857, PR #11928, PR #12091, and PR #12129 added a lot of material on structures, languages, elementary embeddings, and first-order formulas.
Algebra and number theory. There have been contributions in various directions.
- The Cauchy integral formula (PR #10000, last month) unlocked elementary complex analysis, and now the applications are coming quickly. This month saw PR #11864 (the Cauchy-Goursat theorem for an annulus), PR #12095 (Liouville's theorem), and PR #12050 (the maximum modulus principle).
- A particularly exciting application of the complex analysis work is PR #11916, Gelfand's formula for the spectral radius of an element of a Banach algebra. This is proved by considering the resolvent as a holomorphic function with values in the Banach algebra.
- PR #12123 gives the Bochner integral with respect to a measure with density
Geometry: PR #12236, the culmination of a series of PRs, defines the oriented angle between vectors in an oriented two-dimensional vector space.
Combinatorics. The Lubell-Yamamoto-Meshalkin inequalities were added in PR #11248. With PR #4259, another entry was added to the list of 100 theorems in Lean, namely the partition theorem.