This month in mathlib (Jun 2022)
We apologize for the delay in posting this overview. In June 2022 there were 460 PRs merged into mathlib. We list some of the highlights below.

Functional analysis
 PR #14135 proves compactness of the character space of a normed algebra. This is a key step in developing the continuous functional calculus.
 PR #8112 proves the KreinMilman theorem for real normed spaces: any compact convex set is the closure of the convex hull of its extreme points.
 PR #14677 proves Stone's separation theorem: in a vector space over a linearly ordered field, for any pair of disjoint convex subsets, one can partition the whole space into two convex subsets containing the given sets. This is a generalization of the geometric HahnBanach theorem where the partition is made of halfspaces.

Measure theory and probability
 PR #14578 characterizes weak convergence of finite measures in terms of integrals of bounded continuous realvalued functions.
 PR #14755 introduces moments and moment generating function of a real random variable.
 PR #13592 solves the Ballot problem: if in an election, candidate A receives $p$ votes whereas candidate B receives $q$ votes where $p > q$ then the probability that candidate A is strictly ahead throughout the count is $(p  q) / (p + q)$.

Model theory
 PR #14758 proves the Łoś–Vaught Test.

Number theory and group theory

Linear algebra
 PR #14231 reformulates the spectral theorem in terms of matrices.

Tactics
 The
linear_combination
tactic became more powerful in PR #14229 by allowing combinations of arbitrary proofs.
 The