mathlib documentation

algebraic_geometry.function_field

Function field of integral schemes #

We define the function field of an irreducible scheme as the stalk of the generic point. This is a field when the scheme is integral.

Main definition #

The function field of an irreducible scheme is the local ring at its generic point. Despite the name, this is a field only when the scheme is integral.