From 2d907f8539ec0572cc7fc4f7a3d5023a5960acd4 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 28 Jul 2026 06:58:24 +0000 Subject: [PATCH] chore: bump mathlib to 5b3f719: fix(LinearAlgebra/Matrix/Notation): fix defeq abuse in lemmas (#42090) (2026-07-27) --- 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 eafbfb10..d48aa575 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6c5a9081e9b704f0d366214e1fd5e68e1538a4b2", + "rev": "5b3f719bf129e3cf48daf6ff76a2ec5cb6e9b1e3", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "6c5a9081e9b704f0d366214e1fd5e68e1538a4b2", + "inputRev": "5b3f719bf129e3cf48daf6ff76a2ec5cb6e9b1e3", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/verso", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0a7a0cdc42f531e02361cb303b8cbf0e7d334f82", + "rev": "d60e6444e6fd881dfa077ff36e96de75753afa28", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index f4a6607c..c6214de6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -17,7 +17,7 @@ rev = "main" [[require]] name = "mathlib" scope = "leanprover-community" -rev = "6c5a9081e9b704f0d366214e1fd5e68e1538a4b2" +rev = "5b3f719bf129e3cf48daf6ff76a2ec5cb6e9b1e3" [[lean_lib]] name = "LeanMachineLearning"