  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 given norm on $K$, with an explicit description. As
an application, we extend the $p$-adic norm on the field $\mathbb{Q}_p$ of
$p$-adic numbers to its algebraic closure $\mathbb{Q}_p^{\text{alg}}$, and we
define the field $\mathbb{C}_p$ of $p$-adic complex numbers as the completion
of the latter with respect to the $p$-adic norm. Building on the definition of
$\mathbb{C}_p$, we formalize the definition of the Fontaine period ring
$B_{\text{HT}}$ and discuss some applications to the theory of Galois
representations and to $p$-adic Hodge theory. The results formalized in this
paper are a prerequisite to formalize Local Class Field Theory, which is a
fundamental ingredient of the proof of Fermat's Last Theorem.
