From 0cf0aeda75dc654e5cf1665d5f57458a9189589e Mon Sep 17 00:00:00 2001
From: 4hma4d <ahmadalkhalawi@gmail.com>
Date: Fri, 8 Nov 2024 16:56:33 +0300
Subject: [PATCH 1/2] Proved theorem

---
 .../FiniteAdeleRing/BaseChange.lean            | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 3097a39c..06da79e6 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -36,9 +36,21 @@ 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
+  obtain ⟨ι, u, hi⟩ := FiniteDimensional.exists_is_basis_integral A K L
+  have: DecidableEq { x // x ∈ ι } := by exact Classical.typeDecidableEq { x // x ∈ ι }
+  have h := integralClosure_le_span_dualBasis u hi
+  let V := (Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) u)))
+  have hb: B ≃ₐ[A] (integralClosure A L) :=
+    IsIntegralClosure.equiv A B L (integralClosure A L)
+  have h2: IsNoetherian A V := by
+    refine isNoetherian_span_of_finite A ?hA
+    exact Set.finite_range ⇑((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) u)
+  have h3: Module.Finite A (integralClosure A L) := by
+    refine (@Module.Finite.iff_fg A L _ _ _ (Subalgebra.toSubmodule (integralClosure A L))).mpr ?_
+    exact (@isNoetherian_submodule A L _ _ _ V).mp h2 (Subalgebra.toSubmodule (integralClosure A L)) h
+  apply @Module.Finite.equiv A (integralClosure A L) B
+  exact AlgEquiv.toLinearEquiv (AlgEquiv.symm hb)
 
 /-
 In this generality there's a natural isomorphism `L ⊗[K] 𝔸_K^∞ → 𝔸_L^∞` .

From fc590453af74200cf9d4873b46f692ba8a0343a1 Mon Sep 17 00:00:00 2001
From: 4hma4d <ahmadalkhalawi@gmail.com>
Date: Sat, 9 Nov 2024 20:02:25 +0300
Subject: [PATCH 2/2] shortened proof

---
 .../FiniteAdeleRing/BaseChange.lean              | 16 ++--------------
 1 file changed, 2 insertions(+), 14 deletions(-)

diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
index 06da79e6..208f688e 100644
--- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
+++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -37,20 +37,8 @@ variable [IsDomain B]
 variable [Algebra.IsIntegral A B]
 
 example: Module.Finite A B := by
-  obtain ⟨ι, u, hi⟩ := FiniteDimensional.exists_is_basis_integral A K L
-  have: DecidableEq { x // x ∈ ι } := by exact Classical.typeDecidableEq { x // x ∈ ι }
-  have h := integralClosure_le_span_dualBasis u hi
-  let V := (Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) u)))
-  have hb: B ≃ₐ[A] (integralClosure A L) :=
-    IsIntegralClosure.equiv A B L (integralClosure A L)
-  have h2: IsNoetherian A V := by
-    refine isNoetherian_span_of_finite A ?hA
-    exact Set.finite_range ⇑((Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) u)
-  have h3: Module.Finite A (integralClosure A L) := by
-    refine (@Module.Finite.iff_fg A L _ _ _ (Subalgebra.toSubmodule (integralClosure A L))).mpr ?_
-    exact (@isNoetherian_submodule A L _ _ _ V).mp h2 (Subalgebra.toSubmodule (integralClosure A L)) h
-  apply @Module.Finite.equiv A (integralClosure A L) B
-  exact AlgEquiv.toLinearEquiv (AlgEquiv.symm hb)
+  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^∞` .