The properties of a graded Noetherian ring. #
This file proves that the 0-th grade of a Noetherian ring is also a Noetherian ring.
instance
GradedRing.GradeZero.isNoetherianRing
{ι : Type u_1}
{A : Type u_2}
{σ : Type u_3}
[Ring A]
[IsNoetherianRing A]
[DecidableEq ι]
[CanonicallyOrderedAddCommMonoid ι]
[SetLike σ A]
[AddSubgroupClass σ A]
(𝒜 : ι → σ)
[GradedRing 𝒜]
:
IsNoetherianRing ↥(𝒜 0)
If the internally graded ring A is Noetherian, then 𝒜 0 is a Noetherian ring.