Minor idiomatic changes

ImperialCollegeLondon · Dec 4, 2024 · 8fe9043 · 8fe9043
1 parent 7cddfad
commit 8fe9043
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean b/FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean
@@ -462,8 +462,7 @@ noncomputable def FiniteAdeleRing.baseChange : FiniteAdeleRing A K →ₐ[K] Fin
     simp_rw [h]
     simp only [map_add]
     rfl
-  commutes' := by
-    intro r
+  commutes' r := by
     refine ext B L ?_
     have h : (((algebraMap K (FiniteAdeleRing A K)) r) : ProdAdicCompletions A K) =
       (algebraMap K (ProdAdicCompletions A K)) r := rfl