feat(algebra/direct_sum_graded): a direct_sum formed of powers of a submodule of an algebra inherits a ring structure (#6550)
feat(algebra/direct_sum_graded): a direct_sum formed of powers of a submodule of an algebra inherits a ring structure (#6550)

This also fixes some incorrect universe parameters to the `of_submodules` constructors.





leanprover-community/mathlib,leanprover-community/mathlib