From 31370e744f1e22f3eed9114d6b565810acf975b0 Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Fri, 21 Feb 2025 13:46:50 +0100
Subject: [PATCH] bump

---
 FltRegular/NumberTheory/SystemOfUnits.lean | 2 +-
 lake-manifest.json                         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean
index 1c262d71..72300f18 100644
--- a/FltRegular/NumberTheory/SystemOfUnits.lean
+++ b/FltRegular/NumberTheory/SystemOfUnits.lean
@@ -52,7 +52,7 @@ lemma finrank_spanA {R : ℕ} (f : Fin R → G) (hf : LinearIndependent A f) :
   classical
   letI := Fact.mk hp
   have := finrank_span_set_eq_card' (R := A) (Set.range f)
-    ((linearIndependent_subtype_range hf.injective).mpr hf)
+    ((linearIndepOn_id_range_iff hf.injective).mpr hf)
   simp only [Set.toFinset_range, Finset.card_image_of_injective _ hf.injective, card_fin] at this
   rw [← CyclotomicIntegers.powerBasis_dim, ← PowerBasis.finrank']
   conv_rhs => rw [← this]
diff --git a/lake-manifest.json b/lake-manifest.json
index a86a8771..c97fa143 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cb9cedc7509d78c55f43c1adc104296b638eacbe",
+   "rev": "f4084b19bfc93dfa43f54a16be771f883239b9ee",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,