feat(ring_theory/graded_algebra): `mv_polynomial` is ℕ-graded

[jjaassoonn]

---

• [x] depends on: #10113
• [x] depends on: #10115

[eric-wieser]

This likely overlaps a lot with #8913; once the dependencies clear up, we should compare the approaches.

[eric-wieser]

I think you might have pushed to the wrong PR; this no longer resembles a statement about mv_polynomial.

[jjaassoonn]

I think you might have pushed to the wrong PR; this no longer resembles a statement about mv_polynomial.

Yes, I think I reverted it now. Apparently I didn't

[jjaassoonn]

This likely overlaps a lot with #8913; once the dependencies clear up, we should compare the approaches.

The two induction lemmas in #8913 seems very useful. The map mv_polynomial sigma R \to \Oplus i, homogensou_submodule sigma R in this pr isn't very informative.

[eric-wieser]

I merged master to make the diff smaller

[leanprover-community-bot-assistant]

This PR/issue depends on:

• ~~leanprover-community/mathlib#10113~~
• ~~leanprover-community/mathlib#10115~~ By Dependent Issues (🤖). Happy coding!