FunctionFields Material on algebraic function fields of one variable in Lean/Mathlib Notes This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.