diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 3097a39..208f688 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -36,9 +36,9 @@ variable [IsDomain B]
 -- example : Algebra.IsIntegral A B := IsIntegralClosure.isIntegral_algebra A L
 variable [Algebra.IsIntegral A B]
 
--- I can't find in mathlib the assertion that B is a finite A-moduie.
--- It should follow from L/K finite.
-example : Module.Finite A B := by sorry -- I assume this is correct
+example: Module.Finite A B := by
+  have := IsIntegralClosure.isNoetherian A K L B
+  exact Module.IsNoetherian.finite A B
 
 /-
 In this generality there's a natural isomorphism `L ⊗[K] 𝔸_K^∞ → 𝔸_L^∞` .