Commit 2022-04-21 12:09 0821eef1

feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398) If we have a graded ring A and some element f of A, the the localised ring A away from f has a degree zero part. This construction is useful because proj locally is spec of degree zero part of some localised ring. Perhaps this ring belongs to some other file or different name, suggestions are very welcome