I have this project with the aim of formalizing the Modrel-Weil Theorem with LEAN code. This project has been conducted with the help and advice of Dr Marc Masdeu (from UAB).

This project has not been finished yet, but you can see the repository code here.