diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 2fd17060..6ecd3312 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -17,6 +17,10 @@ are defined. In this file we define the natural `K`-algebra map `𝔸_K^∞ →
 the natural `L`-algebra map `𝔸_K^∞ ⊗[K] L → 𝔸_L^∞`, and show that the latter map
 is an isomorphism.
 
+## Main definition
+
+* `FiniteAdeleRing.baseChangeEquiv : L ⊗[K] FiniteAdeleRing A K ≃ₐ[L] FiniteAdeleRing B L`
+
 -/
 
 open scoped Multiplicative
@@ -48,10 +52,6 @@ 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^∞` .
--/
-
 -- We start by filling in some holes in the API for finite extensions of Dedekind domains.
 namespace IsDedekindDomain