Material on algebraic function fields of one variable in Lean/Mathlib
Since there is ongoing work in TauCeti including what was planned here (and much more), this project is no longer active and now archived.
This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.