Formalization of Mazur-Tate-Teitelbaum and Kriz-Nordentoft

This is a Github repo containing formalizations of the following number theory results:

• Mazur, Tate and Teitelbaum's construction of the standard p-adic L-function for GL(2);
• Kriz and Nordentoft's new work on "horizontal p-adic L-functions".