From 70e161cf9f3e8cde9c7861aff17c5ee67dd64bb2 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sun, 11 Oct 2026 21:45:57 +0000 Subject: [PATCH] chore: bump mathlib to 051bc08: chore(Order/SuccPred/Relation): use `to_dual` (#44412) (2026-10-11) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7b29f88..8dcdfd1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1f414401f69059aa7eead47b53ee40bd38455eeb", + "rev": "051bc081081f2bb77b81d47ee69146c4cef28bbe", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "1f414401f69059aa7eead47b53ee40bd38455eeb", + "inputRev": "051bc081081f2bb77b81d47ee69146c4cef28bbe", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lakefile.toml b/lakefile.toml index 4e9caaf..b8562dc 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -13,7 +13,7 @@ weak.linter.mathlibStandardSet = true [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "1f414401f69059aa7eead47b53ee40bd38455eeb" +rev = "051bc081081f2bb77b81d47ee69146c4cef28bbe" [[require]] name = "subverso"