This month in mathlib (Dec 2021)
December 2021 saw 565 commits to mathlib, which sets a new record. In this post we highlight some of these contributions.
 Combinatorics.
 PR #10287 defines graph colorings and partitions.
 PR #10981 defines the concepts of walks, paths, cycles in graph theory.
 PR #10509 defines SalemSpencer sets and Roth numbers.
 Commutative algebra.
 There is now a systematic way to talk about local properties of rings and ring homomorphisms. PR #10734 and PR #10775 prove that being reduced, finite or of finite type are local properties.
 PR #9888 does not introduce new mathematics, but introduces a new way that makes it exceedingly easy to apply lemmas about group homomorphisms to a ring homomorphism (or a linear map, or an algebra homomorphism, etc).
 Algebraic topology.
 Geometry
 PR #10733 shows that an integral scheme is reduced and irreducible. That a scheme is reduced iff its stalks are reduced is shown in PR #10879.

PR #8611 defines the action of
SL(2, ℤ)
on the upper half plane and partially classifies its orbits.  PR #10306 defines orientations of modules and rays in modules. This will be useful in particular in order to define oriented angles in Euclidean plane geometry.
 General topology
 PR #10967 defines uniform convergence on compact subsets for maps from a topological space to a uniform space (for instance a metric space or a topological group). It also shows that the underlying topology is the compactopen topology.
 PR #10914 introduces the specialization order for topological spaces as well as the notion of generic points and sober spaces. Then PR #10989 and PR #11040 show that schemes are sober.
 PR #10701 proves the Tietze extension theorem.
 Functional analysis
 PR #10825 defines the adjoint of a continuous linear map between Hilbert spaces, made possible by the semilinear map refactor, and PR #10837 uses this to put a $C^\ast$algebra structure on the continuous linear maps on a Hilbert space.
 PR #10322 proves continuous bounded realvalued functions form a normed vector lattice.
 PR #10663 proves the BanachSteinhaus theorem.
 PR #9836 adds polar sets in preparation for the BanachAlaoglu theorem.
 Measure theory, integration and probability
 PR #11035 proves one can cover a set in a real vector by balls with controlled measure. This continues the preparation for differentiation of measures.
 PR #10906 define integration on circles in the complex plane. This is foundational material for complex analysis. Important applications will follow very soon.
 PR #10625 defines martingales, and PR #10710 adds super/submartingales.