Formalization of Eichler-Shimura, Mazur-Tate-Teitelbaum, and Kriz-Nordentoft

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

• theory of modular curves and Eichler-Shimura isomorphisms, extracted from Anthropic FLT formalization;
• 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".