From 7cddfad06a28345883d7b80eb73b84d9e015c9b6 Mon Sep 17 00:00:00 2001 From: WilliamCoram Date: Wed, 4 Dec 2024 14:55:07 +0000 Subject: [PATCH] Cleaning --- FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index b7437db4..8b07f9b7 100644 --- 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]