chore: defer a lemma, to avoid needing Cardinal in LinearIndependent (#19626)

Author: kim-em

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -15,6 +15,8 @@ the forgetful functor from `R`-modules to types.
 -/
 
 
+assert_not_exists Cardinal
+
 noncomputable section
 
 open CategoryTheory

Mathlib/Analysis/Convex/Cone/Basic.lean

@@ -39,6 +39,7 @@ While `Convex 𝕜` is a predicate on sets, `ConvexCone 𝕜 E` is a bundled con
 
 assert_not_exists NormedSpace
 assert_not_exists Real
+assert_not_exists Cardinal
 
 open Set LinearMap
 

Mathlib/Analysis/LocallyConvex/Polar.lean

@@ -34,7 +34,6 @@ any bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, where `𝕜` is a no
 polar
 -/
 
-
 variable {𝕜 E F : Type*}
 
 open Topology

Mathlib/LinearAlgebra/Dimension/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl, Sander Dahmen, Kim Morrison
 -/
 import Mathlib.LinearAlgebra.LinearIndependent
+import Mathlib.SetTheory.Cardinal.Basic
 
 /-!
 # Dimension of modules and vector spaces

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -29,6 +29,19 @@ attribute [local instance] nontrivial_of_invariantBasisNumber
 
 open Basis Cardinal Function Module Set Submodule
 
+/-- If every finite set of linearly independent vectors has cardinality at most `n`,
+then the same is true for arbitrary sets of linearly independent vectors.
+-/
+theorem linearIndependent_bounded_of_finset_linearIndependent_bounded {n : ℕ}
+    (H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) :
+    ∀ s : Set M, LinearIndependent R ((↑) : s → M) → #s ≤ n := by
+  intro s li
+  apply Cardinal.card_le_of
+  intro t
+  rw [← Finset.card_map (Embedding.subtype s)]
+  apply H
+  apply linearIndependent_finset_map_embedding_subtype _ li
+
 theorem rank_le {n : ℕ}
     (H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) :
     Module.rank R M ≤ n := by

Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

@@ -19,7 +19,6 @@ This file contains results on the `R`-module structure on functions of finite su
 noncomputable section
 
 open Set LinearMap Submodule
-open scoped Cardinal
 
 universe u v w
 

Mathlib/LinearAlgebra/FreeModule/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Data.Finsupp.Fintype
 import Mathlib.Data.Matrix.Defs
 import Mathlib.LinearAlgebra.Basis.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basis
+import Mathlib.Logic.Small.Basic
 
 /-!
 # Free modules
@@ -37,6 +38,10 @@ variable [Semiring R] [AddCommMonoid M] [Module R M]
 class Module.Free : Prop where
   exists_basis : Nonempty <| (I : Type v) × Basis I R M
 
+theorem Module.free_iff_set : Module.Free R M ↔ ∃ S : Set M, Nonempty (Basis S R M) :=
+  ⟨fun h => ⟨Set.range h.exists_basis.some.2, ⟨Basis.reindexRange h.exists_basis.some.2⟩⟩,
+    fun ⟨S, hS⟩ => ⟨nonempty_sigma.2 ⟨S, hS⟩⟩⟩
+
 /-- If `M` fits in universe `w`, then freeness is equivalent to existence of a basis in that
 universe.
 
@@ -49,10 +54,6 @@ theorem Module.free_def [Small.{w,v} M] :
       ⟨(Basis.reindexRange h.exists_basis.some.2).reindex (equivShrink _)⟩⟩,
     fun h => ⟨(nonempty_sigma.2 h).map fun ⟨_, b⟩ => ⟨Set.range b, b.reindexRange⟩⟩⟩
 
-theorem Module.free_iff_set : Module.Free R M ↔ ∃ S : Set M, Nonempty (Basis S R M) :=
-  ⟨fun h => ⟨Set.range h.exists_basis.some.2, ⟨Basis.reindexRange h.exists_basis.some.2⟩⟩,
-    fun ⟨S, hS⟩ => ⟨nonempty_sigma.2 ⟨S, hS⟩⟩⟩
-
 variable {R M}
 
 theorem Module.Free.of_basis {ι : Type w} (b : Basis ι R M) : Module.Free R M :=

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -7,7 +7,6 @@ import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Data.Set.Subsingleton
 import Mathlib.Lean.Expr.ExtraRecognizers
 import Mathlib.LinearAlgebra.Prod
-import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Module
@@ -82,13 +81,12 @@ linearly dependent, linear dependence, linearly independent, linear independence
 
 -/
 
+assert_not_exists Cardinal
 
 noncomputable section
 
 open Function Set Submodule
 
-open Cardinal
-
 universe u' u
 
 variable {ι : Type u'} {ι' : Type*} {R : Type*} {K : Type*}
@@ -402,18 +400,6 @@ theorem linearIndependent_finset_map_embedding_subtype (s : Set M)
   obtain ⟨b, _hb, rfl⟩ := hy
   simp only [f, imp_self, Subtype.mk_eq_mk]
 
-/-- If every finite set of linearly independent vectors has cardinality at most `n`,
-then the same is true for arbitrary sets of linearly independent vectors.
--/
-theorem linearIndependent_bounded_of_finset_linearIndependent_bounded {n : ℕ}
-    (H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) :
-    ∀ s : Set M, LinearIndependent R ((↑) : s → M) → #s ≤ n := by
-  intro s li
-  apply Cardinal.card_le_of
-  intro t
-  rw [← Finset.card_map (Embedding.subtype s)]
-  apply H
-  apply linearIndependent_finset_map_embedding_subtype _ li
 
 section Subtype
 

Mathlib/RingTheory/TensorProduct/Free.lean

@@ -22,6 +22,8 @@ and deducde that `Module.Free` is stable under base change.
 
 -/
 
+assert_not_exists Cardinal
+
 suppress_compilation
 
 open scoped TensorProduct