Let K be a eld complete with respect to a nonarchimedean real-valued
norm, and let L=K be an algebraic extension. We formalize in Lean 3 the
proof that there is a unique norm on L extending the given norm on K, and
we provide an explicit description of this norm. This is a prerequisite to
formalize Local Class Field Theory, which is an essential component in the
proof of Fermat's Last Theorem.
As an application, we extend the p-adic norm on the eld Qp of p-adic
numbers to its algebraic closure Qalg
p , and we de ne the eld Cp, a p-adic
analogue of the complex numbers.
Building on the de nition of Cp, we formalize the de nition of the
Fontaine period ring BHT. Both Cp and BHT can be used to detect cer-
tain properties of Galois representations.
1Imperial College London / Universidad Autonoma de Madrid
Copyright. All Rights Reserved.