Does the homogeneousSubmodule form a graded ring?

Stream: mathlib4

[Pan Lin]

The document says that:

instance MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring{σ : Type u_1} {R : Type u_3} [CommSemiring R] :
SetLike.GradedMonoid (MvPolynomial.homogeneousSubmodule σ R)

The homogeneous submodules form a graded ring. This instance is used by [DirectSum.commSemiring](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/DirectSum/Ring.html#DirectSum.commSemiring) and DirectSum.algebra.

But why there is no instance DirectSum.Decomposition (MvPolynomial.homogeneousSubmodule σ R) to make the instance GradedRing (MvPolynomial.homogeneousSubmodule σ R)?

[Eric Wieser]

(to write links with a code title, you want [`code`](link) not `[code](link)` )

[Eric Wieser]

(Or just remove the links, I don't think they're helping here)

[Eric Wieser]

(speculating: Ctrl+Shift+V lets you paste into zulip without keeping the unwanted formatting)

[Riccardo Brasca]

#14225 does it

[Pan Lin]

Riccardo Brasca 发言道：

#14225 does it

How can I use it?

[Johan Commelin]

That PR is waiting for its author to process some review comments. Hopefully it will be merged into mathlib soon.