diff --git a/Mathlib.lean b/Mathlib.lean
index 46435bff45d62..763cc291ce207 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -334,6 +334,7 @@ import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Bilinear
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.Submodule.LinearMap
+import Mathlib.Algebra.Module.Submodule.Localization
 import Mathlib.Algebra.Module.Submodule.Map
 import Mathlib.Algebra.Module.Submodule.Pointwise
 import Mathlib.Algebra.Module.Torsion
@@ -2394,6 +2395,7 @@ import Mathlib.LinearAlgebra.Dimension.Finite
 import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.LinearAlgebra.Dimension.Free
 import Mathlib.LinearAlgebra.Dimension.LinearMap
+import Mathlib.LinearAlgebra.Dimension.Localization
 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean
index b480f37b8f1b6..001b5e0e4a2aa 100644
--- a/Mathlib/Algebra/Module/LocalizedModule.lean
+++ b/Mathlib/Algebra/Module/LocalizedModule.lean
@@ -551,7 +551,11 @@ variable {R : Type*} [CommSemiring R] (S : Submonoid R)
 
 variable {M M' M'' : Type*} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M'']
 
-variable [Module R M] [Module R M'] [Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'')
+variable {A : Type*} [CommSemiring A] [Algebra R A] [Module A M'] [IsLocalization S A]
+
+variable [Module R M] [Module R M'] [Module R M''] [IsScalarTower R A M']
+
+variable (f : M →ₗ[R] M') (g : M →ₗ[R] M'')
 
 /-- The characteristic predicate for localized module.
 `IsLocalizedModule S f` describes that `f : M ⟶ M'` is the localization map identifying `M'` as
@@ -1045,6 +1049,14 @@ theorem mk_eq_mk' (s : S) (m : M) :
     LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]
 #align is_localized_module.mk_eq_mk' IsLocalizedModule.mk_eq_mk'
 
+variable (A) in
+lemma mk'_smul_mk' (x : R) (m : M) (s t : S) :
+    IsLocalization.mk' A x s • mk' f m t = mk' f (x • m) (s * t) := by
+  apply smul_injective f (s * t)
+  conv_lhs => simp only [smul_assoc, mul_smul, smul_comm t]
+  simp only [mk'_cancel', map_smul, Submonoid.smul_def s]
+  rw [← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul]
+
 variable (S)
 
 theorem eq_zero_iff {m : M} : f m = 0 ↔ ∃ s' : S, s' • m = 0 :=
@@ -1089,10 +1101,6 @@ theorem mkOfAlgebra {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Al
 
 end Algebra
 
-variable {A : Type*}
-  [CommSemiring A] [Algebra R A] [Module A M'] [IsScalarTower R A M'] [IsLocalization S A]
-
-
 /-- If `(f : M →ₗ[R] M')` is a localization of modules, then the map
 `(localization S) × M → N, (s, m) ↦ s • f m` is the tensor product (insomuch as it is the universal
 bilinear map).
diff --git a/Mathlib/Algebra/Module/Submodule/Localization.lean b/Mathlib/Algebra/Module/Submodule/Localization.lean
new file mode 100644
index 0000000000000..6f569a31bf13f
--- /dev/null
+++ b/Mathlib/Algebra/Module/Submodule/Localization.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.Algebra.Module.LocalizedModule
+
+/-!
+# Localization of Submodules
+
+Results about localizations of submodules and quotient modules are provided in this file.
+
+## Main result
+- `Submodule.localized`:
+  The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`.
+- `Submodule.toLocalized`:
+  The localization map of a submodule `M' →ₗ[R] M'.localized p`.
+- `Submodule.toLocalizedQuotient`:
+  The localization map of a quotient module `M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ M'.localized p`.
+
+## TODO
+- Statements regarding the exactness of localization.
+- Connection with flatness.
+
+-/
+
+open nonZeroDivisors
+
+universe u u' v v'
+
+variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'}
+variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M]
+variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N]
+variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f]
+variable (hp : p ≤ R⁰)
+
+variable (M' : Submodule R M)
+
+/-- Let `S` be the localization of `R` at `p` and `N` be the localization of `M` at `p`.
+This is the localization of an `R`-submodule of `M` viewed as an `S`-submodule of `N`. -/
+def Submodule.localized' : Submodule S N where
+  carrier := { x | ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x }
+  add_mem' := fun {x} {y} ⟨m, hm, s, hx⟩ ⟨n, hn, t, hy⟩ ↦ ⟨t • m + s • n, add_mem (M'.smul_mem t hm)
+    (M'.smul_mem s hn), s * t, by rw [← hx, ← hy, IsLocalizedModule.mk'_add_mk']⟩
+  zero_mem' := ⟨0, zero_mem _, 1, by simp⟩
+  smul_mem' := fun r x h ↦ by
+    have ⟨m, hm, s, hx⟩ := h
+    have ⟨y, t, hyt⟩ := IsLocalization.mk'_surjective p r
+    exact ⟨y • m, M'.smul_mem y hm, t * s, by simp [← hyt, ← hx, IsLocalizedModule.mk'_smul_mk']⟩
+
+/-- The localization of an `R`-submodule of `M` at `p` viewed as an `Rₚ`-submodule of `Mₚ`. -/
+abbrev Submodule.localized : Submodule (Localization p) (LocalizedModule p M) :=
+  M'.localized' (Localization p) p (LocalizedModule.mkLinearMap p M)
+
+/-- The localization map of a submodule. -/
+@[simps!]
+def Submodule.toLocalized' : M' →ₗ[R] M'.localized' S p f :=
+  f.restrict (q := (M'.localized' S p f).restrictScalars R) (fun x hx ↦ ⟨x, hx, 1, by simp⟩)
+
+/-- The localization map of a submodule. -/
+abbrev Submodule.toLocalized : M' →ₗ[R] M'.localized p :=
+  M'.toLocalized' (Localization p) p (LocalizedModule.mkLinearMap p M)
+
+instance Submodule.isLocalizedModule : IsLocalizedModule p (M'.toLocalized' S p f) where
+  map_units x := by
+    simp_rw [Module.End_isUnit_iff]
+    constructor
+    · exact fun _ _ e ↦ Subtype.ext
+        (IsLocalizedModule.smul_injective f x (congr_arg Subtype.val e))
+    · rintro m
+      use (IsLocalization.mk' S 1 x) • m
+      rw [Module.algebraMap_end_apply, ← smul_assoc, IsLocalization.smul_mk'_one,
+        IsLocalization.mk'_self', one_smul]
+  surj' := by
+    rintro ⟨y, x, hx, s, rfl⟩
+    exact ⟨⟨⟨x, hx⟩, s⟩, by ext; simp⟩
+  exists_of_eq e := by simpa [Subtype.ext_iff] using
+      IsLocalizedModule.exists_of_eq (S := p) (f := f) (congr_arg Subtype.val e)
+
+/-- The localization map of a quotient module. -/
+def Submodule.toLocalizedQuotient' : M ⧸ M' →ₗ[R] N ⧸ M'.localized' S p f :=
+  Submodule.mapQ M' ((M'.localized' S p f).restrictScalars R) f (fun x hx ↦ ⟨x, hx, 1, by simp⟩)
+
+/-- The localization map of a quotient module. -/
+abbrev Submodule.toLocalizedQuotient : M ⧸ M' →ₗ[R] LocalizedModule p M ⧸ M'.localized p :=
+  M'.toLocalizedQuotient' (Localization p) p (LocalizedModule.mkLinearMap p M)
+
+@[simp]
+lemma Submodule.toLocalizedQuotient'_mk (x : M) :
+    M'.toLocalizedQuotient' S p f (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x) := rfl
+
+open Submodule Submodule.Quotient IsLocalization in
+instance IsLocalizedModule.toLocalizedQuotient' (M' : Submodule R M) :
+    IsLocalizedModule p (M'.toLocalizedQuotient' S p f) where
+  map_units x := by
+    refine (Module.End_isUnit_iff _).mpr ⟨fun m n e ↦ ?_, fun m ↦ ⟨(IsLocalization.mk' S 1 x) • m,
+        by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]⟩⟩
+    obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
+    simp only [Module.algebraMap_end_apply, ← mk_smul, Submodule.Quotient.eq, ← smul_sub] at e
+    replace e := Submodule.smul_mem _ (IsLocalization.mk' S 1 x) e
+    rwa [smul_comm, ← smul_assoc, smul_mk'_one, mk'_self', one_smul, ← Submodule.Quotient.eq] at e
+  surj' y := by
+    obtain ⟨y, rfl⟩ := mk_surjective _ y
+    obtain ⟨⟨y, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f y
+    exact ⟨⟨Submodule.Quotient.mk y, s⟩,
+      by simp only [Function.uncurry_apply_pair, toLocalizedQuotient'_mk, ← mk_smul, mk'_cancel']⟩
+  exists_of_eq {m n} e := by
+    obtain ⟨⟨m, rfl⟩, n, rfl⟩ := PProd.mk (mk_surjective _ m) (mk_surjective _ n)
+    obtain ⟨x, hx, s, hs⟩ : f (m - n) ∈ _ := by simpa [Submodule.Quotient.eq] using e
+    obtain ⟨c, hc⟩ := exists_of_eq (S := p) (show f (s • (m - n)) = f x by simp [-map_sub, ← hs])
+    exact ⟨c * s, by simpa only [← Quotient.mk_smul, Submodule.Quotient.eq,
+      ← smul_sub, mul_smul, hc] using M'.smul_mem c hx⟩
+
+instance (M' : Submodule R M) : IsLocalizedModule p (M'.toLocalizedQuotient p) :=
+  IsLocalizedModule.toLocalizedQuotient' _ _ _ _
diff --git a/Mathlib/Algebra/Module/Zlattice.lean b/Mathlib/Algebra/Module/Zlattice.lean
index 7170d23b8fccd..9d269b8ddb54d 100644
--- a/Mathlib/Algebra/Module/Zlattice.lean
+++ b/Mathlib/Algebra/Module/Zlattice.lean
@@ -464,7 +464,7 @@ theorem Zlattice.rank : finrank ℤ L = finrank K E := by
         Finset.sdiff_eq_empty_iff_subset] at h
       replace h := Finset.card_le_card h
       rwa [not_lt, h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span,
-        finrank_span_set_eq_card _ ht_lin]
+        finrank_span_set_eq_card ht_lin]
     -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction
     suffices ¬ LinearIndependent ℤ (fun x : ↥(insert v (Set.range e)) => (x : E)) by
       contrapose! this
@@ -500,6 +500,6 @@ theorem Zlattice.rank : finrank ℤ L = finrank K E := by
   · -- To prove that `finrank K E ≤ finrank ℤ L`, we use the fact `b` generates `E` over `K`
     -- and thus `finrank K E ≤ card b = finrank ℤ L`
     rw [← topEquiv.finrank_eq, ← h_spanE]
-    convert finrank_span_le_card (K := K) (Set.range b)
+    convert finrank_span_le_card (R := K) (Set.range b)
 
 end Zlattice
diff --git a/Mathlib/LinearAlgebra/Dimension/Constructions.lean b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
index 6fb253c151ca6..197d36f64b5e9 100644
--- a/Mathlib/LinearAlgebra/Dimension/Constructions.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Constructions.lean
@@ -374,27 +374,6 @@ theorem FiniteDimensional.finrank_tensorProduct :
 
 end TensorProduct
 
-section Span
-
-variable [StrongRankCondition R]
-
-theorem rank_span_le_of_finite {s : Set M} (hs : s.Finite) : Module.rank R (span R s) ≤ #s := by
-  rw [Module.rank_def]
-  apply ciSup_le'
-  rintro ⟨t, ht⟩
-  letI := hs.fintype
-  simpa [Cardinal.mk_image_eq Subtype.val_injective] using linearIndependent_le_span' _
-    (ht.map (f := Submodule.subtype _) (by simp)).image s (fun x ↦ by aesop)
-
-theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card := by
-  simpa using rank_span_le_of_finite s.finite_toSet
-
-theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ :=
-  (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _)
-#align rank_span_of_finset rank_span_of_finset
-
-end Span
-
 section SubmoduleRank
 
 section
@@ -449,9 +428,93 @@ theorem Submodule.finrank_le_finrank_of_le {s t : Submodule R M} [Module.Finite
 
 end
 
-
 end SubmoduleRank
 
+section Span
+
+variable [StrongRankCondition R]
+
+theorem rank_span_le (s : Set M) : Module.rank R (span R s) ≤ #s := by
+  rw [Finsupp.span_eq_range_total, ← lift_strictMono.le_iff_le]
+  refine (lift_rank_range_le _).trans ?_
+  rw [rank_finsupp_self]
+  simp only [lift_lift, ge_iff_le, le_refl]
+#align rank_span_le rank_span_le
+
+theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card := by
+  simpa using rank_span_le s.toSet
+
+theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ :=
+  (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _)
+#align rank_span_of_finset rank_span_of_finset
+
+open Submodule FiniteDimensional
+
+variable (R)
+
+/-- The rank of a set of vectors as a natural number. -/
+protected noncomputable def Set.finrank (s : Set M) : ℕ :=
+  finrank R (span R s)
+#align set.finrank Set.finrank
+
+variable {R}
+
+theorem finrank_span_le_card (s : Set M) [Fintype s] : finrank R (span R s) ≤ s.toFinset.card :=
+  finrank_le_of_rank_le (by simpa using rank_span_le (R := R) s)
+#align finrank_span_le_card finrank_span_le_card
+
+theorem finrank_span_finset_le_card (s : Finset M) : (s : Set M).finrank R ≤ s.card :=
+  calc
+    (s : Set M).finrank R ≤ (s : Set M).toFinset.card := finrank_span_le_card (M := M) s
+    _ = s.card := by simp
+#align finrank_span_finset_le_card finrank_span_finset_le_card
+
+theorem finrank_range_le_card {ι : Type*} [Fintype ι] (b : ι → M) :
+    (Set.range b).finrank R ≤ Fintype.card ι := by
+  classical
+  refine (finrank_span_le_card _).trans ?_
+  rw [Set.toFinset_range]
+  exact Finset.card_image_le
+#align finrank_range_le_card finrank_range_le_card
+
+theorem finrank_span_eq_card [Nontrivial R] {ι : Type*} [Fintype ι] {b : ι → M}
+    (hb : LinearIndependent R b) :
+    finrank R (span R (Set.range b)) = Fintype.card ι :=
+  finrank_eq_of_rank_eq
+    (by
+      have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb
+      rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
+        lift_eq_nat_iff] at this)
+#align finrank_span_eq_card finrank_span_eq_card
+
+theorem finrank_span_set_eq_card {s : Set M} [Fintype s] (hs : LinearIndependent R ((↑) : s → M)) :
+    finrank R (span R s) = s.toFinset.card :=
+  finrank_eq_of_rank_eq
+    (by
+      have : Module.rank R (span R s) = #s := rank_span_set hs
+      rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this)
+#align finrank_span_set_eq_card finrank_span_set_eq_card
+
+theorem finrank_span_finset_eq_card {s : Finset M} (hs : LinearIndependent R ((↑) : s → M)) :
+    finrank R (span R (s : Set M)) = s.card := by
+  convert finrank_span_set_eq_card (s := (s : Set M)) hs
+  ext
+  simp
+#align finrank_span_finset_eq_card finrank_span_finset_eq_card
+
+theorem span_lt_of_subset_of_card_lt_finrank {s : Set M} [Fintype s] {t : Submodule R M}
+    (subset : s ⊆ t) (card_lt : s.toFinset.card < finrank R t) : span R s < t :=
+  lt_of_le_of_finrank_lt_finrank (span_le.mpr subset)
+    (lt_of_le_of_lt (finrank_span_le_card _) card_lt)
+#align span_lt_of_subset_of_card_lt_finrank span_lt_of_subset_of_card_lt_finrank
+
+theorem span_lt_top_of_card_lt_finrank {s : Set M} [Fintype s]
+    (card_lt : s.toFinset.card < finrank R M) : span R s < ⊤ :=
+  lt_top_of_finrank_lt_finrank (lt_of_le_of_lt (finrank_span_le_card _) card_lt)
+#align span_lt_top_of_card_lt_finrank span_lt_top_of_card_lt_finrank
+
+end Span
+
 section SubalgebraRank
 
 open Module
diff --git a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
index ceaced347eef7..17c19499196ba 100644
--- a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
+++ b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
@@ -59,13 +59,6 @@ theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 (h : Module.rank K V <
   finite_def.2 <| (Basis.ofVectorSpace K V).nonempty_fintype_index_of_rank_lt_aleph0 h
 #align basis.finite_of_vector_space_index_of_rank_lt_aleph_0 Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0
 
--- TODO how far can we generalise this?
-theorem rank_span_le (s : Set V) : Module.rank K (span K s) ≤ #s := by
-  obtain ⟨b, hb, hsab, hlib⟩ := exists_linearIndependent K s
-  convert Cardinal.mk_le_mk_of_subset hb
-  rw [← hsab, rank_span_set hlib]
-#align rank_span_le rank_span_le
-
 theorem rank_quotient_add_rank (p : Submodule K V) :
     Module.rank K (V ⧸ p) + Module.rank K p = Module.rank K V := by
   classical
@@ -326,68 +319,6 @@ open Submodule FiniteDimensional
 
 variable [DivisionRing K] [AddCommGroup V] [Module K V]
 
-variable (K)
-
-/-- The rank of a set of vectors as a natural number. -/
-protected noncomputable def Set.finrank (s : Set V) : ℕ :=
-  finrank K (span K s)
-#align set.finrank Set.finrank
-
-variable {K}
-
-theorem finrank_span_le_card (s : Set V) [Fintype s] : finrank K (span K s) ≤ s.toFinset.card :=
-  finrank_le_of_rank_le (by simpa using rank_span_le (K := K) s)
-#align finrank_span_le_card finrank_span_le_card
-
-theorem finrank_span_finset_le_card (s : Finset V) : (s : Set V).finrank K ≤ s.card :=
-  calc
-    (s : Set V).finrank K ≤ (s : Set V).toFinset.card := finrank_span_le_card (V := V) s
-    _ = s.card := by simp
-#align finrank_span_finset_le_card finrank_span_finset_le_card
-
-theorem finrank_range_le_card {ι : Type*} [Fintype ι] {b : ι → V} :
-    (Set.range b).finrank K ≤ Fintype.card ι := by
-  classical
-  refine (finrank_span_le_card _).trans ?_
-  rw [Set.toFinset_range]
-  exact Finset.card_image_le
-#align finrank_range_le_card finrank_range_le_card
-
-theorem finrank_span_eq_card {ι : Type*} [Fintype ι] {b : ι → V} (hb : LinearIndependent K b) :
-    finrank K (span K (Set.range b)) = Fintype.card ι :=
-  finrank_eq_of_rank_eq
-    (by
-      have : Module.rank K (span K (Set.range b)) = #(Set.range b) := rank_span hb
-      rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
-        lift_eq_nat_iff] at this)
-#align finrank_span_eq_card finrank_span_eq_card
-
-theorem finrank_span_set_eq_card (s : Set V) [Fintype s] (hs : LinearIndependent K ((↑) : s → V)) :
-    finrank K (span K s) = s.toFinset.card :=
-  finrank_eq_of_rank_eq
-    (by
-      have : Module.rank K (span K s) = #s := rank_span_set hs
-      rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this)
-#align finrank_span_set_eq_card finrank_span_set_eq_card
-
-theorem finrank_span_finset_eq_card (s : Finset V) (hs : LinearIndependent K ((↑) : s → V)) :
-    finrank K (span K (s : Set V)) = s.card := by
-  convert finrank_span_set_eq_card (s : Set V) hs
-  ext
-  simp
-#align finrank_span_finset_eq_card finrank_span_finset_eq_card
-
-theorem span_lt_of_subset_of_card_lt_finrank {s : Set V} [Fintype s] {t : Submodule K V}
-    (subset : s ⊆ t) (card_lt : s.toFinset.card < finrank K t) : span K s < t :=
-  lt_of_le_of_finrank_lt_finrank (span_le.mpr subset)
-    (lt_of_le_of_lt (finrank_span_le_card _) card_lt)
-#align span_lt_of_subset_of_card_lt_finrank span_lt_of_subset_of_card_lt_finrank
-
-theorem span_lt_top_of_card_lt_finrank {s : Set V} [Fintype s]
-    (card_lt : s.toFinset.card < finrank K V) : span K s < ⊤ :=
-  lt_top_of_finrank_lt_finrank (lt_of_le_of_lt (finrank_span_le_card _) card_lt)
-#align span_lt_top_of_card_lt_finrank span_lt_top_of_card_lt_finrank
-
 /-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
 dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
 theorem exists_linearIndependent_snoc_of_lt_finrank {n : ℕ} {v : Fin n → V}
@@ -492,7 +423,7 @@ theorem linearIndependent_iff_card_eq_finrank_span {ι : Type*} [Fintype ι] {b
 
 theorem linearIndependent_iff_card_le_finrank_span {ι : Type*} [Fintype ι] {b : ι → V} :
     LinearIndependent K b ↔ Fintype.card ι ≤ (Set.range b).finrank K := by
-  rw [linearIndependent_iff_card_eq_finrank_span, finrank_range_le_card.le_iff_eq]
+  rw [linearIndependent_iff_card_eq_finrank_span, (finrank_range_le_card _).le_iff_eq]
 #align linear_independent_iff_card_le_finrank_span linearIndependent_iff_card_le_finrank_span
 
 /-- A family of `finrank K V` vectors forms a basis if they span the whole space. -/
diff --git a/Mathlib/LinearAlgebra/Dimension/Localization.lean b/Mathlib/LinearAlgebra/Dimension/Localization.lean
new file mode 100644
index 0000000000000..d359e5dc57bb6
--- /dev/null
+++ b/Mathlib/LinearAlgebra/Dimension/Localization.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.LinearAlgebra.Dimension.Constructions
+import Mathlib.Algebra.Module.Submodule.Localization
+
+/-!
+# Rank of localization
+
+## Main statements
+
+- `IsLocalizedModule.lift_rank_eq`: `rank_Rₚ Mₚ = rank R M`.
+- `rank_quotient_add_rank_of_isDomain`: The **rank-nullity theorem** for commutative domains.
+
+-/
+open Cardinal nonZeroDivisors
+
+section CommRing
+
+universe u u' v v'
+
+variable {R : Type u} (S : Type u') {M : Type v} {N : Type v'}
+variable [CommRing R] [CommRing S] [AddCommGroup M] [AddCommGroup N] [Module R M]
+variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S N]
+variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f]
+variable (hp : p ≤ R⁰)
+
+lemma IsLocalizedModule.lift_rank_eq :
+    Cardinal.lift.{v} (Module.rank S N) = Cardinal.lift.{v'} (Module.rank R M) := by
+  cases' subsingleton_or_nontrivial R
+  · have := (algebraMap R S).codomain_trivial; simp only [rank_subsingleton, lift_one]
+  have := (IsLocalization.injective S hp).nontrivial
+  apply le_antisymm
+  · rw [Module.rank_def, lift_iSup (bddAbove_range.{v', v'} _)]
+    apply ciSup_le'
+    intro ⟨s, hs⟩
+    choose sec hsec using IsLocalizedModule.surj p f
+    refine LinearIndependent.cardinal_lift_le_rank (ι := s) (v := fun i ↦ (sec i).1) ?_
+    rw [linearIndependent_iff'] at hs ⊢
+    intro t g hg i hit
+    apply hp (sec i).2.prop
+    apply IsLocalization.injective S hp
+    rw [map_zero]
+    refine hs t (fun i ↦ algebraMap R S (g i * (sec i).2)) ?_ _ hit
+    simp only [map_mul, mul_smul, algebraMap_smul, ← Submonoid.smul_def,
+      hsec, ← map_smul, ← map_sum, hg, map_zero]
+  · rw [Module.rank_def, lift_iSup (bddAbove_range.{v, v} _)]
+    apply ciSup_le'
+    intro ⟨s, hs⟩
+    choose sec hsec using IsLocalization.surj p (S := S)
+    refine LinearIndependent.cardinal_lift_le_rank (ι := s) (v := fun i ↦ f i) ?_
+    rw [linearIndependent_iff'] at hs ⊢
+    intro t g hg i hit
+    apply (IsLocalization.map_units S (sec (g i)).2).mul_left_injective
+    classical
+    let u := fun (i : s) ↦ (t.erase i).prod (fun j ↦ (sec (g j)).2)
+    have : f (t.sum fun i ↦ u i • (sec (g i)).1 • i) = f 0
+    · convert congr_arg (t.prod (fun j ↦ (sec (g j)).2) • ·) hg
+      · simp only [map_sum, map_smul, Submonoid.smul_def, Finset.smul_sum]
+        apply Finset.sum_congr rfl
+        intro j hj
+        simp only [← @IsScalarTower.algebraMap_smul R S N, Submonoid.coe_finset_prod, map_prod]
+        rw [← hsec, mul_comm (g j), mul_smul, ← mul_smul, Finset.prod_erase_mul (h := hj)]
+      rw [map_zero, smul_zero]
+    obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := p) this
+    simp_rw [smul_zero, Finset.smul_sum, ← mul_smul, Submonoid.smul_def, ← mul_smul, mul_comm] at hc
+    simp only [hsec, zero_mul, map_eq_zero_iff (algebraMap R S) (IsLocalization.injective S hp)]
+    apply hp (c * u i).prop
+    exact hs t _ hc _ hit
+
+lemma IsLocalizedModule.rank_eq {N : Type v} [AddCommGroup N]
+    [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) [IsLocalizedModule p f] :
+    Module.rank S N = Module.rank R M := by simpa using IsLocalizedModule.lift_rank_eq S p f hp
+
+/-- The **rank-nullity theorem** for commutative domains. -/
+theorem rank_quotient_add_rank_of_isDomain [IsDomain R] (M' : Submodule R M) :
+    Module.rank R (M ⧸ M') + Module.rank R M' = Module.rank R M := by
+  apply lift_injective.{max u v}
+  rw [lift_add, ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (M'.toLocalized R⁰) le_rfl,
+    ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl,
+    ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (M'.toLocalizedQuotient R⁰) le_rfl,
+    ← lift_add, rank_quotient_add_rank]
+
+end CommRing
diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean
index fc9a2847b6041..2c7d5d56fc24d 100644
--- a/Mathlib/NumberTheory/NumberField/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/Basic.lean
@@ -60,6 +60,9 @@ protected theorem isAlgebraic : Algebra.IsAlgebraic ℚ K :=
   Algebra.IsAlgebraic.of_finite _ _
 #align number_field.is_algebraic NumberField.isAlgebraic
 
+instance [NumberField L] [Algebra K L] : FiniteDimensional K L :=
+  Module.Finite.of_restrictScalars_finite ℚ K L
+
 /-- The ring of integers (or number ring) corresponding to a number field
 is the integral closure of ℤ in the number field. -/
 def ringOfIntegers :=