diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean
index e61fdf32557a31..62e906cf932619 100644
--- a/Mathlib/LinearAlgebra/Dimension/Free.lean
+++ b/Mathlib/LinearAlgebra/Dimension/Free.lean
@@ -61,7 +61,10 @@ theorem rank_mul_rank (A : Type v) [AddCommMonoid A]
   convert! lift_rank_mul_lift_rank F K A <;> rw [lift_id]
 
 /-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
-$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. -/
+$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.
+
+See `Module.finrank_mul_finrank'` for a variant over a tower of domains that assumes the rings are
+module-finite rather than the modules being free. -/
 theorem Module.finrank_mul_finrank : finrank F K * finrank K A = finrank F A := by
   simp_rw [finrank]
   rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
diff --git a/Mathlib/RingTheory/Algebraic/Integral.lean b/Mathlib/RingTheory/Algebraic/Integral.lean
index 7d74915b28c242..261982a9854099 100644
--- a/Mathlib/RingTheory/Algebraic/Integral.lean
+++ b/Mathlib/RingTheory/Algebraic/Integral.lean
@@ -5,12 +5,11 @@ Authors: Johan Commelin
 -/
 module
 
+public import Mathlib.Algebra.Ring.Hom.InjSurj
 public import Mathlib.LinearAlgebra.Dimension.Localization
 public import Mathlib.RingTheory.Algebraic.Basic
 public import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
-public import Mathlib.RingTheory.Localization.BaseChange
-
-import Mathlib.RingTheory.Polynomial.Subring
+public import Mathlib.RingTheory.Polynomial.Subring
 
 /-!
 # Algebraic elements and integral elements
@@ -561,6 +560,23 @@ theorem rank_fractionRing [IsDomain S] :
     Module.rank (FractionRing R) (FractionRing S) = Module.rank R S :=
   rank_of_isFractionRing ..
 
+attribute [local instance] FractionRing.liftAlgebra in
+/-- Tower law for `Module.finrank` in a tower of domains `R → S → B` that is module-finite at each
+step. This is a variant of `Module.finrank_mul_finrank` that assumes the rings are domains (and
+module-finite) instead of the modules being free. -/
+theorem _root_.Module.finrank_mul_finrank' (T : Type*) [CommRing T] [IsDomain T] [Algebra S T]
+    [Algebra R T] [IsScalarTower R S T]
+    [FaithfulSMul S T] [Module.Finite R S] [Module.Finite S T] :
+    Module.finrank R S * Module.finrank S T = Module.finrank R T := by
+  have : FaithfulSMul R T := .trans R S T
+  have : IsDomain R := (FaithfulSMul.algebraMap_injective R T).isDomain
+  have : IsDomain S := (FaithfulSMul.algebraMap_injective S T).isDomain
+  have : Module.Finite R T := Module.Finite.trans S T
+  rw [← finrank_of_isFractionRing R (FractionRing R) S (FractionRing S),
+    ← finrank_of_isFractionRing S (FractionRing S) T (FractionRing T),
+    ← finrank_of_isFractionRing R (FractionRing R) T (FractionRing T),
+    Module.finrank_mul_finrank (FractionRing R) (FractionRing S) (FractionRing T)]
+
 end Algebra.IsAlgebraic
 
 section Polynomial