Behaviour of valuations under a finite separable extension

[kbuzzard]

For number fields, and I assume in the "AKLB generality" when L/K is a finite separable extension, the following is true. If w is a finite place of L which pulls back to a finite place v of K, and if i:K -> L denotes the inclusion, then for x in K we have w(x)^e=v(x), where e denotes the ramification index of w over v. I had hoped that this would be easy, but ramification index seems to be defined in huge generality and we will need results specific to Dedekind domains in order to prove this. These results are surely already present in some form in mathlib though, given that we have things like sum of e_i * f_i = [L:K].

The goal is to fill in the sorry in the declaration IsDedekindDomain.HeightOneSpectrum.valuation_comap in the file FLT.DededkindDomain.FiniteAdeleRing.BaseChange.

[kbuzzard]

@erdOne can you claim this issue by just making a comment with the word claim? You have basically done it.

[erdOne]

claim