K_v -> L_w is continuous

[kbuzzard]

We have that it's a K-algebra homomorphism but we also need that it's continuous. This is the sorry in adicCompletionComapAlgHom in the file DedekindDomain.FiniteAdeleRing.BaseChange (line 230 at the time of writing).

[erdOne]

This is

  cont := 
    letI : UniformSpace K := v.adicValued.toUniformSpace;
    letI : UniformSpace L := w.adicValued.toUniformSpace;
    UniformSpace.Completion.continuous_extension

I can open a PR but it might be faster if you just push it.
Edit: I opened a PR.

[kbuzzard]

Thanks!