mathlib

37a8a0b2 - feat(ring_theory/graded_algebra): define homogeneous localisation (#12784)

feat(ring_theory/graded_algebra): define homogeneous localisation (#12784) This pr defines `homogeneous_localization`. For `x` in projective spectrum of `A`, homogeneous localisation at `x` is the subring of $$A_x$$ containing `a/b` where `a` and `b` have the same degree. This construction is mainly used in constructing structure sheaf of Proj of a graded ring