search

ImperialCollegeLondon / FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Apache License 2.0
262 stars 48 forks source link

K_v -> L_w is continuous #235

Open kbuzzard opened 4 days ago

kbuzzard commented 4 days ago

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 commented 3 days ago

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.