2024-06-11 06:47
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): morphism of locally ringed space $\mathrm{Proj}|_{D(f)} -> \mathrm{Spec} A^0_f$ (#13689) …
Added AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection