From 3e178f86c9657fccc5452033b3ec40a8967cb0cf Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 17 Jul 2026 06:52:52 +0000 Subject: [PATCH] chore: bump mathlib to bfefa91: fix(Algebra/MonoidAlgebra/Defs): rename AddMonoidAlgebra.coeff_zero_zero (#41783) (2026-07-17) --- lake-manifest.json | 6 +++--- lakefile.toml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 63f09b5f..e2658e8c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9ff650a05edbad3ca4c9f97a49454fb83ef803fe", + "rev": "bfefa91d21732b8ea21199657680224f37f8e748", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "9ff650a05edbad3ca4c9f97a49454fb83ef803fe", + "inputRev": "bfefa91d21732b8ea21199657680224f37f8e748", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/verso", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "31a49105f960721073a9adfc82b261f5d0f2ce1e", + "rev": "45337c634fbcb2bb22fb45c9847faaa10d4d1b67", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index a113ec90..09dd4769 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -17,7 +17,7 @@ rev = "main" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "9ff650a05edbad3ca4c9f97a49454fb83ef803fe" +rev = "bfefa91d21732b8ea21199657680224f37f8e748" [[lean_lib]] name = "LeanMachineLearning"