This month in mathlib (Aug 2022)
In August 2022 there were 506 PRs merged into mathlib. We list some of the highlights below.

Measure theory.
 PR #15321 adds portmanteau implications concerning open and closed sets.

Algebra.
 PR #15970 proves that a ring morphism is finite if and only if it is integral and of finite_type.
 PR #15736 proves that localization maps of artinian rings are surjective.
 PR #16047 defines the module of Kähler differentials.
 PR #14742 defines the principal unit group of a valuation subring and proves some basic properties.
 PR #15030 defines divisible groups.
 PR #16144 defines the normal closure of a fields extension.

Number theory.
 PR #15316 proves that $[S/P^e : R/p] = e \cdot [S/P : R/p]$, where $e$ is the ramification index of an extension of Dedekind domains $R \hookrightarrow S$ and $P$ is an ideal over $p$.
 PR #12287 proves the fundamental identity of ramification index and inertia degree.
 PR #16171 gives a new proof of quadratic reciprocity, using Gauss sums.
 PR #15230 defines $2$torsion polynomials of an elliptic curve.

Representation theory.

Topology.

Probability theory.

Algebraic and differential geometry.

Linear algebra.
 PR #15220 proves the existence of the LDL decomposition.

Category theory.

Logic/order theory.
 PR #15305 defines Heyting algebras.

Recreational mathematics.
 PR #15279 solves the Königsberg bridges problem.
During this month, we also got three new versions of Lean, including 3.47.0 which backported the Lean 4 field notation logic, allowing to get rid of many explicit projections for extending classes.