chore: Reorganize results about rank and finrank. (#9349)

The files `Mathlib.LinearAlgebra.FreeModule.Rank`, `Mathlib.LinearAlgebra.FreeModule.Finite.Rank`, `Mathlib.LinearAlgebra.Dimension` and `Mathlib.LinearAlgebra.Finrank` were reorganized into a
folder `Mathlib.LinearAlgebra.Dimension`, containing the following files
- `Basic.lean`: Contains the definition of `Module.rank`.
- `Finrank.lean`: Contains the definition of `FiniteDimensional.finrank`.
- `StrongRankCondition.lean`: Contains results about `rank` and `finrank`
      over rings satisfying strong rank condition
- `Free.lean`: Contains results about `rank` and `finrank` of free modules
- `Finite.lean`: Contains conditions or consequences for `rank` to be finite or zero
- `Constructions.lean`: Contains the calculation of the `rank` of various constructions.
- `DivisionRing.lean`: Contains results about `rank` and `finrank` of spaces over division rings.
- `LinearMap.lean`: Contains results about `LinearMap.rank`

API changes:
`IsNoetherian.rank_lt_aleph0` and `FiniteDimensional.rank_lt_aleph0` are replaced with
`rank_lt_aleph0`.
`Module.Free.finite_basis` was renamed to `Module.Finite.finite_basis`.
`FiniteDimensional.finrank_eq_rank` was renamed to `finrank_eq_rank`.
`rank_eq_cardinal_basis` and `rank_eq_cardinal_basis'` were removed 
in favour of `Basis.mk_eq_mk` and `Basis.mk_eq_mk''`.



Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib.lean

@@ -2383,7 +2383,14 @@ import Mathlib.LinearAlgebra.Contraction
 import Mathlib.LinearAlgebra.CrossProduct
 import Mathlib.LinearAlgebra.DFinsupp
 import Mathlib.LinearAlgebra.Determinant
-import Mathlib.LinearAlgebra.Dimension
+import Mathlib.LinearAlgebra.Dimension.Basic
+import Mathlib.LinearAlgebra.Dimension.Constructions
+import Mathlib.LinearAlgebra.Dimension.DivisionRing
+import Mathlib.LinearAlgebra.Dimension.Finite
+import Mathlib.LinearAlgebra.Dimension.Finrank
+import Mathlib.LinearAlgebra.Dimension.Free
+import Mathlib.LinearAlgebra.Dimension.LinearMap
+import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 import Mathlib.LinearAlgebra.Dual
@@ -2395,19 +2402,16 @@ import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
 import Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.LinearAlgebra.FiniteSpan
-import Mathlib.LinearAlgebra.Finrank
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.FinsuppVectorSpace
 import Mathlib.LinearAlgebra.FreeAlgebra
 import Mathlib.LinearAlgebra.FreeModule.Basic
 import Mathlib.LinearAlgebra.FreeModule.Determinant
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
-import Mathlib.LinearAlgebra.FreeModule.Finite.Rank
 import Mathlib.LinearAlgebra.FreeModule.IdealQuotient
 import Mathlib.LinearAlgebra.FreeModule.Norm
 import Mathlib.LinearAlgebra.FreeModule.PID
-import Mathlib.LinearAlgebra.FreeModule.Rank
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.InvariantBasisNumber

Mathlib/Algebra/Category/ModuleCat/Free.lean

@@ -3,13 +3,8 @@ Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
-import Mathlib.Algebra.Category.ModuleCat.Abelian
-import Mathlib.Algebra.Category.ModuleCat.Adjunctions
+import Mathlib.LinearAlgebra.Dimension.Finite
 import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
-import Mathlib.LinearAlgebra.FreeModule.Basic
-import Mathlib.LinearAlgebra.FreeModule.Finite.Rank
-import Mathlib.LinearAlgebra.Dimension
-import Mathlib.LinearAlgebra.Finrank
 
 /-!
 # Exact sequences with free modules
@@ -179,6 +174,6 @@ theorem free_shortExact_finrank_add [Module.Free R S.X₁] [Module.Free R S.X₃
     FiniteDimensional.finrank R S.X₂ = n + p := by
   apply FiniteDimensional.finrank_eq_of_rank_eq
   rw [free_shortExact_rank_add hS', ← hN, ← hP]
-  simp only [Nat.cast_add, FiniteDimensional.finrank_eq_rank]
+  simp only [Nat.cast_add, finrank_eq_rank]
 
 end ModuleCat

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.Algebra.DirectSum.Module
+import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.Eigenspace.Basic
 import Mathlib.LinearAlgebra.Trace
 

Mathlib/Algebra/Lie/Weights/Linear.lean

@@ -5,6 +5,7 @@ Authors: Oliver Nash
 -/
 import Mathlib.Algebra.Lie.Weights.Basic
 import Mathlib.LinearAlgebra.Trace
+import Mathlib.LinearAlgebra.FreeModule.PID
 
 /-!
 # Lie modules with linear weights

Mathlib/Algebra/LinearRecurrence.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
 import Mathlib.Data.Polynomial.Eval
-import Mathlib.LinearAlgebra.Dimension
+import Mathlib.LinearAlgebra.Dimension.Constructions
 
 #align_import algebra.linear_recurrence from "leanprover-community/mathlib"@"039a089d2a4b93c761b234f3e5f5aeb752bac60f"
 

Mathlib/Algebra/Quaternion.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Algebra.Equiv
-import Mathlib.LinearAlgebra.Finrank
+import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.LinearAlgebra.FreeModule.Basic
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.SetTheory.Cardinal.Ordinal

Mathlib/Analysis/NormedSpace/Connected.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.Convex.Topology
-import Mathlib.LinearAlgebra.Dimension
+import Mathlib.LinearAlgebra.Dimension.DivisionRing
 import Mathlib.Topology.Algebra.Module.Cardinality
 
 /-!

Mathlib/Data/Matrix/Rank.lean

@@ -3,13 +3,9 @@ Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Eric Wieser
 -/
-import Mathlib.LinearAlgebra.FreeModule.Finite.Rank
-import Mathlib.LinearAlgebra.Matrix.ToLin
-import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.LinearAlgebra.Matrix.DotProduct
 import Mathlib.LinearAlgebra.Determinant
 import Mathlib.LinearAlgebra.Matrix.Diagonal
-import Mathlib.Data.Complex.Module
 
 #align_import data.matrix.rank from "leanprover-community/mathlib"@"17219820a8aa8abe85adf5dfde19af1dd1bd8ae7"
 

Mathlib/FieldTheory/Finiteness.lean

@@ -3,8 +3,7 @@ Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.RingTheory.Finiteness
-import Mathlib.LinearAlgebra.Dimension
+import Mathlib.LinearAlgebra.Dimension.DivisionRing
 
 #align_import field_theory.finiteness from "leanprover-community/mathlib"@"039a089d2a4b93c761b234f3e5f5aeb752bac60f"
 
@@ -43,11 +42,8 @@ theorem iff_rank_lt_aleph0 : IsNoetherian K V ↔ Module.rank K V < ℵ₀ := by
 
 variable (K V)
 
-/-- The dimension of a noetherian module over a division ring, as a cardinal,
-is strictly less than the first infinite cardinal `ℵ₀`. -/
-theorem rank_lt_aleph0 : ∀ [IsNoetherian K V], Module.rank K V < ℵ₀ :=
-  @IsNoetherian.iff_rank_lt_aleph0.1
-#align is_noetherian.rank_lt_aleph_0 IsNoetherian.rank_lt_aleph0
+@[deprecated] protected alias rank_lt_aleph0 := _root_.rank_lt_aleph0
+#align is_noetherian.rank_lt_aleph_0 rank_lt_aleph0
 
 variable {K V}
 

Mathlib/FieldTheory/MvPolynomial.lean

@@ -3,9 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import Mathlib.Data.MvPolynomial.CommRing
-import Mathlib.LinearAlgebra.Dimension
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.RingTheory.MvPolynomial.Basic
 
 #align_import field_theory.mv_polynomial from "leanprover-community/mathlib"@"039a089d2a4b93c761b234f3e5f5aeb752bac60f"

Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Group.Equiv.TypeTags
-import Mathlib.Algebra.Module.Equiv
-import Mathlib.Data.Finsupp.Defs
 import Mathlib.GroupTheory.FreeAbelianGroup
 import Mathlib.GroupTheory.FreeGroup.IsFreeGroup
-import Mathlib.LinearAlgebra.Dimension
+import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 
 #align_import group_theory.free_abelian_group_finsupp from "leanprover-community/mathlib"@"47b51515e69f59bca5cf34ef456e6000fe205a69"
 

Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean

@@ -36,6 +36,11 @@ namespace LinearMap
 
 section Basic
 
+attribute [-instance] instCoeOut
+
+attribute [local instance 2000] RingHomClass.toNonUnitalRingHomClass
+attribute [local instance 2000] NonUnitalRingHomClass.toMulHomClass MulHomClass.toFunLike
+
 /-- `charpoly f` is the characteristic polynomial of the matrix of `f` in any basis. -/
 @[simp]
 theorem charpoly_toMatrix {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) :