Ostrowski's Theorem

The goal of this project is to formalize a proof of Ostrowski's Theorem for Q and for function fields of the form K(X).

This project is part of the 2022 Xena Summer Workshop, held at Imperial College London from September 26th to September 30th, 2022.

Project Leader: María Inés de Frutos-Fernández

Project Members:

• Alistair Bill
• Billy Miao
• Michał Mrugała
• Jan Ot Piña

Installation instructions

The formalization has been developed over Lean 3 and its matemathical library mathlib. For detailed instructions to install Lean, mathlib, and supporting tools, visit the Lean Community website.

After installation, run the command leanproject get mariainesdff/ostrowski to obtain a copy of the project's source files and dependencies. To open the project in VS Code, either run path/to/ostrowski on the command line, or use the "Open Folder" menu option to open the project's root directory.

Copyright (C) 2022, María Inés de Frutos-Fernández