chore(LinearAlgebra/Dimension): split off rank_quotient_eq_of_le_torsion (#18730)

This result doesn't seem to be used in Mathlib and it pulls in many imports such as the theory of the ring `ZMod`, which we should not need to define finite dimensional spaces.




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Author: Vierkantor

Mathlib.lean

@@ -3159,6 +3159,7 @@ import Mathlib.LinearAlgebra.Dimension.LinearMap
 import Mathlib.LinearAlgebra.Dimension.Localization
 import Mathlib.LinearAlgebra.Dimension.RankNullity
 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
+import Mathlib.LinearAlgebra.Dimension.Torsion
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 import Mathlib.LinearAlgebra.Dual

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl, Sander Dahmen, Kim Morrison, Chris Hughes, Anne Baanen
 -/
 import Mathlib.LinearAlgebra.Dimension.Free
-import Mathlib.Algebra.Module.Torsion
 
 /-!
 # Rank of various constructions
@@ -75,20 +74,6 @@ theorem rank_quotient_add_rank_le [Nontrivial R] (M' : Submodule R M) :
 theorem rank_quotient_le (p : Submodule R M) : Module.rank R (M ⧸ p) ≤ Module.rank R M :=
   (mkQ p).rank_le_of_surjective Quot.mk_surjective
 
-theorem rank_quotient_eq_of_le_torsion {R M} [CommRing R] [AddCommGroup M] [Module R M]
-    {M' : Submodule R M} (hN : M' ≤ torsion R M) : Module.rank R (M ⧸ M') = Module.rank R M :=
-  (rank_quotient_le M').antisymm <| by
-    nontriviality R
-    rw [Module.rank]
-    have := nonempty_linearIndependent_set R M
-    refine ciSup_le fun ⟨s, hs⟩ ↦ LinearIndependent.cardinal_le_rank (v := (M'.mkQ ·)) ?_
-    rw [linearIndependent_iff'] at hs ⊢
-    simp_rw [← map_smul, ← map_sum, mkQ_apply, Quotient.mk_eq_zero]
-    intro t g hg i hi
-    obtain ⟨r, hg⟩ := hN hg
-    simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at hg
-    exact r.prop _ (mul_comm (g i) r ▸ hs t _ hg i hi)
-
 end Quotient
 
 section ULift

Mathlib/LinearAlgebra/Dimension/Torsion.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.Algebra.Module.Torsion
+import Mathlib.LinearAlgebra.Dimension.Constructions
+
+/-!
+# Rank and torsion
+
+## Main statements
+
+- `rank_quotient_eq_of_le_torsion` : `rank M/N = rank M` if `N ≤ torsion M`.
+-/
+
+open Submodule
+
+theorem rank_quotient_eq_of_le_torsion {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
+    {M' : Submodule R M} (hN : M' ≤ torsion R M) : Module.rank R (M ⧸ M') = Module.rank R M :=
+  (rank_quotient_le M').antisymm <| by
+    nontriviality R
+    rw [Module.rank]
+    have := nonempty_linearIndependent_set R M
+    refine ciSup_le fun ⟨s, hs⟩ ↦ LinearIndependent.cardinal_le_rank (v := (M'.mkQ ·)) ?_
+    rw [linearIndependent_iff'] at hs ⊢
+    simp_rw [← map_smul, ← map_sum, mkQ_apply, Quotient.mk_eq_zero]
+    intro t g hg i hi
+    obtain ⟨r, hg⟩ := hN hg
+    simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at hg
+    exact r.prop _ (mul_comm (g i) r ▸ hs t _ hg i hi)

Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean

@@ -9,6 +9,7 @@ import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.Quotient.Pi
 import Mathlib.RingTheory.Ideal.Basis
 import Mathlib.LinearAlgebra.Dimension.Constructions
+import Mathlib.Data.ZMod.Quotient
 
 /-! # Ideals in free modules over PIDs