This month in mathlib (Jul 2022)
In July 2022 there were 611 PRs merged into mathlib. We list some of the highlights below.

Arithmetic
 PR #15091 defines Bézout rings and PR #15424 proves that Bezout domains are integrally closed. PR #15109 proves the same for GCD domains.
 PR #14717 proves Wilson's Theorem.
 PR #15315 proves $[Frac(S):Frac(R)] = [S/pS:R/p]$for a Dedekind domain $R$ and its integral closure $S$ and maximal ideal $p$. This is the first step in showing the fundamental identity of inertia degree and ramification index.
 PR #8002 proves Bertrand's postulate.

Algebraic geometry and commutative algebra
 PR #15487 proves the affine communication lemma.
 PR #14944 introduces a basic framework for classes of morphisms between schemes. Examples are provided by PR #15379 (finite type is a local property), PR #15427 (finite ring morphisms are stable under base change), and PR #15243 (formally étale/smooth/unramified morphisms are stable under base change).
 PR #15089 defines the Rees algebra of an ideal.
 PR #12895 adds injective modules and Baer's criterion.

Group theory

Noncommutative or nonassociative algebra
 PR #14348 defines the Ore localization of a ring (a noncommutative analogue of the usual localization).
 PR #14790 gives the universal property and isomorphisms for the even subalgebra of a Clifford algebra.
 PR #14179 characterises Cartan subalgebras as limiting values of upper central series.
 PR #11073 introduces Jordan rings.

Topology and functional analysis

Probability and measure theory

Combinatorics
 In additive combinatorics, PR #14697 proves Ruzsa's covering lemma: for finite sets $s$ and $t$ in a commutative group, we can cover $s$ with at most $s + t/ t$ copies of $t  t$. PR #14070 introduces Behrend's construction and PR #15327 establish Behrend's lower bound on Roth numbers.
 In combinatorics of families of finite sets, PR #14497 proves the HarrisKleitman inequality and PR #14543 proves Kleitman's bound.
 In graph theory, PR #15158 proves Euler's condition for trails.

Computability theory and information theory

Tactics

PR #14878 brings
polyrith
, a tactic using Sage to solve polynomial equalities with hypotheses.

PR #14878 brings