Skip to main content

This month in mathlib (Jul 2022)

Source

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

    • PR #8632 proves that groups of order $p^2$ are commutative.
    • PR #15402 proves that a finitely generated torsion abelian group is finite.

  • Non-commutative or non-associative algebra

    • PR #14348 defines the Ore localization of a ring (a non-commutative 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

    • PR #14965 introduces Noetherian spaces.
    • PR #15124 proves that in a normed space, a set is von Neumann bounded if and only if it is bounded in the metric sense.
    • PR #15055 proves the Hellinger-Toeplitz theorem: if a symmetric operator is defined everywhere, then it is automatically continuous.

  • Probability and measure theory

    • PR #14737 proves Doob's maximal inequality for non-negative submartingales.
    • PR #14909 proves the discrete stochastic integral of a submartingale is a submartingale.
    • PR #15106 computes gaussian integrals.
    • PR #15129 establishes Chernoff's bound on the upper/lower tail of a real random variable.

  • 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 Harris-Kleitman inequality and PR #14543 proves Kleitman's bound.
    • In graph theory, PR #15158 proves Euler's condition for trails.

  • Computability theory and information theory

    • PR #14739 introduces the Hamming distance and norm.
    • PR #15505 proves the Ackermann function isn't primitive recursive.

  • Tactics

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