The lemma with the (weird) name IsDedekindDomain.HeightOneSpectrum.v_adicCompletionComapAlgHom says that in the usual AKLB situation, if x is in K_v then w(x : L_w) = v(x)^e. We have this in the global setting, it's valuation_comap in the same file (FLT.DedekindDomain.FiniteAdeleRing.BaseChange).
@erdOne are you working on this in #229 or were you planning on leaving it sorried? Someone should also change the name (it's not about an AlgHom).
The lemma with the (weird) name
IsDedekindDomain.HeightOneSpectrum.v_adicCompletionComapAlgHomsays that in the usual AKLB situation, if x is in K_v then w(x : L_w) = v(x)^e. We have this in the global setting, it'svaluation_comapin the same file (FLT.DedekindDomain.FiniteAdeleRing.BaseChange).@erdOne are you working on this in #229 or were you planning on leaving it sorried? Someone should also change the name (it's not about an AlgHom).