Commit 2023-12-02 07:05 75641abe

View on Github →

chore: bump Mathlib to Lean v4.4.0-rc1 (#8781) The commits below are all approved PRs, as planned, except:

  • the second last one which resolves conflicts in lake-manifest.json and lean-toolchain.
  • the last one the reverts a mysterious change in Mathlib.Analysis.Seminorm, discussed in the comment below.

Estimated changes