From db1deea45a51d850f2b8cd51f3f8e96a8c4d1885 Mon Sep 17 00:00:00 2001 From: WilliamCoram Date: Wed, 4 Dec 2024 16:39:25 +0000 Subject: [PATCH] Update FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Co-authored-by: Kevin Buzzard --- FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean index af522928..848c8075 100644 --- a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean +++ b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean @@ -437,7 +437,7 @@ noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] Fin toFun ak := ⟨ProdAdicCompletions.baseChange A K L B ak.1, (ProdAdicCompletions.baseChange_isFiniteAdele_iff A K L B ak).1 ak.2⟩ map_one' := by - refine ext B L ?_ + ext have h : (1 : FiniteAdeleRing A K) = (1 : ProdAdicCompletions A K) := rfl have t : (1 : FiniteAdeleRing B L) = (1 : ProdAdicCompletions B L) := rfl simp_rw [h,t]