This month in mathlib (Nov 2021)
This post summarizes some of the activity that happened in mathlib in November.

Geometry and algebraic topology.
 The series
PR #10284,
PR #10297,
PR #10303,
PR #10328,
PR #10334,
and PR #10401
constructs the sheafification of presheaves with respect to
a Grothendieck topology on a category, culminating with a construction
of colimits in the category
SheafedSpace
. It is an important building block in setting up algebraic geometry, as well as a requirement for the Liquid Tensor Experiment (LTE). A corollary is that the category of sheaves with values in a suitable concrete abelian category is itself an abelian category. This has been formalised for LTE, and should appear in mathlib in the near future.  Barycentric coordinates have been further studied in a series of PRs including for instance PR #10320 relating them to determinants.
 PR #10381 proves the orthogonal group is generated by reflections.

PR #10195
defines the fundamental groupoid, as functor from
Top
toGroupoid
.
 The series
PR #10284,
PR #10297,
PR #10303,
PR #10328,
PR #10334,
and PR #10401
constructs the sheafification of presheaves with respect to
a Grothendieck topology on a category, culminating with a construction
of colimits in the category

Number theory.
 PR #9071 defines the class number of number fields and function fields. This finishes the finiteness proof of the class group of a number field and function field, described in a previous blog post.
 PR #8820 adds Lucas primality test.

Group theory.

Combinatorics.
 PR #10029 proves Hindman's theorem on finite sums.
 Set families are making their way to mathlib with PR #9926, PR #10223, PR #10238 respectively defining antichains, shadow of a set family, UV compression. Those are ingredients for the LYM inequality, Sperner's theorem and the KruskalKatona theorem.

Linear algebra and functional analysis
 The sequence of PRs PR #9840, PR #9995, PR #10317 establishes the connection between eigenvalues and the Rayleigh quotient, and proves the diagonalization theorem for selfadjoint endomorphisms on finitedimensional inner product spaces.
 PR #10145 introduces $C^*$algebras.
 PR #10530 proves properties of spectrum in a Banach algebra.
 PR #9097 defines the Minkowski gauge functional.

Analysis
 PR #9791 proves the PicardLindelöf/CauchyLipschitz theorem about ordinary differential equations.

PR #10057 defines Vitali families
and PR #10101
shows the main theorem on differentiation of measures:
given two measures
ρ
andμ
on a finitedimensional real vector space, the ratioρ (ball x r) / μ (ball x r)
convergesμ
almost everywhere to the RadonNikodym derivative ofρ
with respect toμ
whenr
tends to0
. The theorem is in fact proved in the more general context of Vitali families, as in Federer's famous book on geometric measure theory.  PR #10073 proves convergence of a sequence which does not oscillate infinitely.
 PR #10258 proves that, if $u_n$ is subadditive, then $u_n / n$ converges.