feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring

[FMLJohn]

trafficstars

---

[FMLJohn]

I have proved that for a Noetherian graded ring, its 0th grade is also a Noetherian ring.

[FMLJohn]

@kbuzzard @eric-wieser

[joneugster]

bench!

[joneugster]

This PR has approving reviews by both @eric-wieser and @kbuzzard, and superficially it seems to me that there's nothing speaking against a merge.

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by joneugster.

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 15798830fa1b69df9c43ba6933bad469928d1d6c. There were no significant changes against commit 730684c92655a41b391fa63c5a2717a26e201d95.

[mattrobball]

Let's merge master on this before sending it off at least.

[github-actions[bot]]

PR summary 0d00dd9305

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.GradedMonoid	402	407	+5 (+1.24%)

---

Declarations diff

+ GradeZero.isNoetherianRing + GradedRing.coe_projZeroRingHom'_apply + GradedRing.projZeroRingHom' + GradedRing.projZeroRingHom'_apply_coe + GradedRing.projZeroRingHom'_surjective + coe_algebraMap + coe_intCast + coe_mul + coe_natCast + coe_ofNat + coe_one + coe_pow + instAlgebra + instCommMonoid + instCommRing + instCommSemiring + instMonoid + instRing + instSemiring + subalgebra + submonoid + subring + subsemiring

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 0d00dd9305dc69d957802214c218438d20a4234a. There were significant changes against commit 9c4c6f78c9a1b7beba018504e284d497a3761af2:

  Benchmark   Metric    Change
  ============================
- build       linting     5.1%

[mattrobball]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style