Cleaning

ImperialCollegeLondon · Dec 4, 2024 · 7cddfad · 7cddfad
1 parent 176751c
commit 7cddfad
Showing 1 changed file with 0 additions and 9 deletions.
diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -478,15 +478,6 @@ noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] Fin
     simp_rw [j]
     exact IsScalarTower.algebraMap_apply K L (ProdAdicCompletions B L) r
 
-
-    -- How can I coerce r into L - without using algebraMap?
-    -- this is cleary true, just need to show it
-
-
-
-
-
-
 -- Presumably we have this?
 noncomputable def bar {K L AK AL : Type*} [CommRing K] [CommRing L]
     [CommRing AK] [CommRing AL] [Algebra K AK] [Algebra K AL] [Algebra K L]