Commit 2022-03-13 00:04 9f1f8c13
View on Github →feat(ring_theory/graded_algebra/homogeneous_ideal): definition of irrelevant ideal of a graded algebra (#12548)
For an ℕ-graded ring ⨁ᵢ 𝒜ᵢ, the irrelevant ideal refers to ⨁_{i>0} 𝒜ᵢ.
This construction is used in the Proj construction in algebraic geometry.