Finite extension of a local field has the obvious topology

[kbuzzard]

The explicit result we need is this: if L/K is a finite extension of number fields, and if w is a place of L above v a place of K, then L_w when considered as a K_v-algebra has the module topology. There will shortly be a proof in the LaTeX (the maths proof is: L_w is finite-dimensional over K_v because its dimension is at most [L:K], and the w-adic norm is a norm on a finite-dimensional space over a complete field so it's equivalent to the product norm after you pick a basis, and so the w-adic topology must be the product topology, which is the module topology.

The declaration is IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_isModuleTopology, in FLT.DedekindDomain.FiniteAdeleRing.BaseChange.