bump

leanprover-community · Feb 21, 2025 · 31370e7 · 31370e7
1 parent 1370d9b
commit 31370e7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cb9cedc7509d78c55f43c1adc104296b638eacbe",
+   "rev": "f4084b19bfc93dfa43f54a16be771f883239b9ee",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,