From 64dd5ec070ec2aada0ae07eb739b4f09c9078556 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Mon, 21 Oct 2024 09:58:48 +0100
Subject: [PATCH] state hard theorem

---
 FLT/NumberField/AdeleRing.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
index 58a3e90..ad5f766 100644
--- a/FLT/NumberField/AdeleRing.lean
+++ b/FLT/NumberField/AdeleRing.lean
@@ -104,3 +104,10 @@ noncomputable def ProdAdicCompletions.baseChange :
   map_add' := sorry
   map_smul' := sorry
 }
+
+-- hard but hopefully enough (this proof will be a lot of work)
+theorem ProdAdicCompletions.baseChange_iso (x : ProdAdicCompletions (𝓞 K) K) :
+  ProdAdicCompletions.IsFiniteAdele x ↔
+  ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChange K L (1 ⊗ₜ x)) := sorry
+
+-- Can we now write down the isomorphism L ⊗ 𝔸_K^∞ = 𝔸_L^∞ ?