Formalizing Norm Extensions and Applications to Number Theory

María Inés de Frutos-Fernández

Let $K$ be a field complete with respect to a nonarchimedean real-valued norm, and let $L/K$ be an algebraic extension. We show that there is a unique norm on $L$ extending the giv…