Valuation is commutative with Galois group action

Stream: Is there code for X?

[Junjie Bai]

Has anyone show that the valuation is commutative with Galois group action under the assumption that the field is complete? i.e. If L/K is finite Galois ValExtension and K is complete, then v_L(x) = v_L(s (x)) for all s in Galois group.

[María Inés de Frutos Fernández]

I did this in terms of norms, see docs#spectralNorm_eq_of_equiv. I think it should not be too hard to translate to valuations, using the normed/valued dictionary.

[Junjie Bai]

Thanks a lot!

[Junjie Bai]

Sorry, I find it hard for me to translate this to valuations. I try to use 'spectralNorm_unique' to proof it, but this theorem need a AlgebraNorm and the norm over L induced by valuation seems not to be a AlgebraNorm of K. Should I proof this in another way?