mathlib3

9f1f8c13 - feat(ring_theory/graded_algebra/homogeneous_ideal): definition of irrelevant ideal of a graded algebra (#12548)

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.