Skip to main content

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.

    • PR #15501 shows that $k[G^{n + 1}]$ is free over $k[G]$.
    • PR #15822 defines Young diagrams.
  • Topology.

    • PR #15965 defines locally connected spaces and proves some basic properties.
    • PR #15999 defines quasi-separated topological spaces.
  • Probability theory.

    • PR #14933 proves Doob's upcrossing estimate.
    • PR #15904 proves the a.e. martingale convergence theorem.
    • PR #16042 proves the $L^1$ martingale convergence theorem and Lévy's upwards theorem.
  • Algebraic and differential geometry.

    • PR #15667 proves that any holomorphic function on a compact connected manifold is constant.
    • PR #16059 allows to define a property of a scheme morphism from the corresponding ring homomorphism property.
  • Linear algebra.

    • PR #15220 proves the existence of the LDL decomposition.
  • Category theory.

    • PR #15987 proves the Special Adjoint Functor Theorem
    • PR #16246 proves that the normalized Moore complex is homotopy equivalent to the alternating face map complex.
  • Logic/order theory.

  • 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.