mathlib documentation

algebraic_geometry.Spec

$Spec R$ as a LocallyRingedSpace #

We bundle the structure_sheaf R construction for R : CommRing as a LocallyRingedSpace.

Future work #

Make it a functor.